proposition: Fact binomial_sym n p : p <= n -> binomial n p = binomial n (n-p).
proof: Proof. intros H; do 2 (rewrite binomial_le; try lia). rewrite Nat.mul_comm; do 3 f_equal; lia. Qed.
imports: Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd)