proposition: Fact binomial_le n p : p <= n -> binomial n p = div (fact n) (fact p * fact (n-p)).
proof: Proof. intros H. symmetry; apply div_prop with (r := 0). + rewrite binomial_thm with (p := p); auto; ring. + red; change 1 with (1*1); apply Nat.mul_le_mono; apply fact_gt_0. Qed.
imports: Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd)