nat_choose_succ_mul@{} n m : nat_choose n.+1 m.+1 = (n.+1 * nat_choose n m) / m.+1. Proof. destruct (leq_dichotomy m n) as [H | H]. 2: { rewrite 2 nat_choose_lt; only 2, 3: exact _. rewrite nat_mul_zero_r. symmetry; apply nat_div_zero_l. } rewrite 2 nat_choose_factorial. 2,3: exact _. rewrite nat_div_mul_l. 2: exact _. rewrite nat_div_div_l. by rewrite (nat_mul_comm _ m.+1), nat_mul_assoc. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids