proposition: Theorem binomial_thm n p : p <= n -> fact n = binomial n p * fact p * fact (n-p).
proof: Proof. intros H. replace n with (n-p+p) at 1 2 by lia. generalize (n-p); clear n H; intros n. induction on n p as IH with measure (n+p). revert n p IH; intros [ | n ] [ | p ] IH; simpl plus; auto. + rewrite binomial_nn; simpl; lia. + rewrite Nat.add_0_r, binomial_n0; simpl; lia. + rewrite fact_S, binomial_SS. replace (S (n+S p)) with (S p+S n) by lia. do 3 rewrite Nat.mul_add_distr_r; f_equal. * replace (n+S p) with (S n+p) by lia. rewrite fact_S, IH; try lia; ring. * rewrite (fact_S n), IH; try lia; ring. Qed.
imports: Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd)