nat_choose_one_r@{} n : nat_choose n 1 = n. Proof. induction n as [|n IHn]; only 1: reflexivity. rewrite_refl nat_choose_succ. exact (ap nat_succ IHn). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids