proposition: Lemma binomial_complement n k : k <= n -> binomial n k = binomial n (n - k).
proof: Proof. intros L. pose (x := fact k * fact (n - k)). cut (x * binomial n k = x * binomial n (n - k)). { apply Nat.mul_cancel_l. subst x. apply Nat.neq_mul_0; split; apply fact_neq_0. } subst x. rewrite binomial_factorial; auto. rewrite <-(binomial_factorial n (n - k)). 2:lia. replace (n - (n - k)) with k by lia. ring. Qed.
imports: Arith ZArith String List Psatz Factorial