proposition: Lemma csum_M0lt a b: natp a -> b <> \0c -> a <c a +c b.
proof: Proof. move => aN bnz. move: (cltS aN); rewrite - csum2cr (Nsucc_rw aN) => asa. apply: (clt_leT asa); apply: csum_Meqle; apply: cge1; fprops. by move/card_nonempty. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)