proposition: Lemma binomial_S n k : k <= n -> S n * binomial n k = S k * binomial (S n) (S k).
proof: Proof. intros Hkn. pose (x := fact k * fact (n - k)). pose (y := fact (S k) * fact (S n - S k)). cut (x * y * (S n * binomial n k) = x * y * (S k * binomial (S n) (S k))). { apply Nat.mul_cancel_l. subst x y. do 2 (apply Nat.neq_mul_0; split); apply fact_neq_0. } subst x y. cut ((fact (S k) * fact (S n - S k)) * (S n * (fact k * fact (n - k) * binomial n k)) = fact k * fact (n - k) * (S k * ((fact (S k) * fact (S n - S k)) * binomial (S n) (S k)))). { intros E. etransitivity; [ | etransitivity ]; [ | apply E | ]; ring. } rewrite binomial_factorial. rewrite binomial_factorial. simpl; ring. lia. auto. Qed.
imports: Arith ZArith String List Psatz Factorial