proposition: Lemma binom_symmetric n p: natp n -> p <=c n -> binom n p = binom n (n -c p).
proof: Proof. move => nN h. move: (NS_le_nat h nN) => pN. move: (cdiff_ab_le_a p (CS_nat nN)) => aux. rewrite (binom_pr1 nN pN h) cprodC (binom_pr1 nN (NS_diff p nN) aux). rewrite double_diff //; apply: le_minus. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)