proposition: Lemma cdiv_pr a b: natp a -> natp b -> a = (b *c (a %/c b)) +c (a %%c b).
proof: Proof. move => aN bN. case: (equal_or_not b \0c) => bnz. by rewrite bnz (crem_zero aN) cquo_zero cprod0r Nsum0l. by move: (cdivision aN bN bnz) =>[_ _ [h _]]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)