proposition: Lemma cdiff_nz1 a b: natp a -> natp b -> (csucc b) <=c a -> a -c b <> \0c.
proof: Proof. move=> aN bN /(cleSltP bN) lesba; apply: cdiff_nz => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)