nat_choose_succ_l_diag@{} n : nat_choose n.+1 n = n.+1. Proof. induction n as [|n IHn]; only 1: reflexivity. rewrite_refl nat_choose_succ. rhs_V nrapply (nat_add_comm _ 1). nrapply ap011. - exact IHn. - apply nat_choose_diag. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids