nat_choose_sub@{} n m : m <= n -> nat_choose n m = nat_choose n (n - m). Proof. intros H. rewrite 2 nat_choose_factorial. 2,3: exact _. rewrite nat_sub_sub_cancel_r. 2: exact _. by rewrite nat_mul_comm. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids