proposition: Lemma binomSn0 n: natp n -> binom (csucc n) \0c = \1c.
proof: Proof. move: NS0 => zn nN; rewrite /binom /variant induction_terms // LgV//. by Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)