nat_choose_diag@{} n : nat_choose n n = 1. Proof. induction n as [|n IHn]; only 1: reflexivity. rewrite_refl nat_choose_succ. rhs_V nrapply nat_add_zero_r. nrapply ap011. - exact IHn. - rapply nat_choose_lt. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids