proposition: Lemma binom0 n: natp n -> binom n \0c = \1c.
proof: Proof. move=> nN. case: (equal_or_not n \0c) => nz; first by rewrite nz binom00. move: (cpred_pr nN nz)=> [pN ->]; rewrite binomSn0 //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)