nat_choose_factorial@{} n m : m <= n -> nat_choose n m = factorial n / (factorial m * factorial (n - m)). Proof. revert n m; apply nat_double_ind_leq; intro n. { rewrite nat_mul_one_l. rewrite nat_sub_zero_r. symmetry; rapply nat_div_cancel. } { rewrite nat_sub_cancel. rewrite nat_mul_one_r. rewrite nat_div_cancel. 1: nrapply nat_choose_diag. exact _. } intros m H IHn. rewrite_refl nat_choose_succ. rewrite 2 IHn. 2,3: exact _. rewrite <- (nat_div_cancel_mul_l _ _ m.+1). 2: exact _. rewrite nat_mul_assoc. rewrite <- nat_factorial_succ. rewrite <- (nat_div_cancel_mul_l (factorial n) _ (n - m)). 2: rapply equiv_lt_lt_sub. rewrite nat_mul_assoc. rewrite (nat_mul_comm (n - m) (factorial m.+1)). rewrite <- nat_mul_assoc. rewrite nat_sub_succ_r. rewrite <- nat_factorial_pred. 2: rapply equiv_lt_lt_sub. lhs_V nrapply nat_div_dist. - rewrite nat_factorial_succ. rewrite <- nat_mul_assoc. exact _. - rewrite <- nat_dist_r. rewrite nat_add_succ_l. rewrite nat_add_sub_r_cancel. 2: exact _. rewrite <- nat_factorial_succ. reflexivity. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids