nat_choose_lt@{} n m : n < m -> nat_choose n m = 0. Proof. revert m; induction n; hnf; intros m H; destruct H. 1, 2: reflexivity. 1, 2: rewrite_refl nat_choose_succ; exact (ap011 nat_add (IHn _ _) (IHn _ _)). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids