proposition: Lemma binomial_factorial n k : k <= n -> fact k * fact (n - k) * binomial n k = fact n.
proof: Proof. revert k; induction n; intros [ | k]. - reflexivity. - lia. - intros _. simpl. lia. - intros L. simpl (binomial _ _). rewrite Nat.mul_add_distr_l. replace (fact (S k) * fact (S n - S k) * binomial n k) with ((S k) * (fact k * fact (n - k) * binomial n k)) by (simpl; ring). rewrite IHn. 2:lia. assert (D : k = n \/ k < n) by lia. destruct D as [D | D]. + subst k. rewrite binomial_lt; auto. simpl; ring. + replace (S n - S k) with (S (n - S k)) by lia. replace (fact (S k) * fact (S (n - S k)) * binomial n (S k)) with (S (n - S k) * (fact (S k) * fact (n - S k) * binomial n (S k))) by (simpl; ring). rewrite IHn. 2:lia. rewrite <-Nat.mul_add_distr_r. change (fact (S n)) with (S n * fact n). apply Nat.mul_cancel_r. apply fact_neq_0. lia. Qed.
imports: Arith ZArith String List Psatz Factorial