proposition: Lemma binom_nn n: natp n -> binom n n = \1c.
proof: Proof. move=> nN. rewrite (binom_symmetric nN (cleR (CS_nat nN))) cdiff_nn binom0 =>//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)