proposition: Lemma binom0Sm m: natp m -> binom \0c (csucc m) = \0c.
proof: Proof. move=> mN; have snz := (@succ_nz m). by rewrite /binom /variant induction_term0 LgV//; [ Ytac0 | apply: NS_succ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)