proposition: Lemma cdivision a b (q := a %/c b) (r := a %%c b): natp a -> natp b -> b <> \0c -> [/\ natp q, natp r & cdivision_prop a b q r].
proof: Proof. move=> aN bN bnz. pose pr z := (a <c b *c (csucc z)). have pa: pr a by apply /(cleSltP aN);rewrite cprodC; apply: Nprod_M1le; fprops. case: (least_int_prop aN pa). rewrite /pr - /(cquo_internal _ _) - cquoE. move => qN qa qb. have rv: r = a -c b *c q by rewrite/r cremE. have rN: natp r by rewrite rv; apply: NS_diff => //; apply: NS_prod. split => //. apply /cdivision_prop_alt=> //; split => //. case: (equal_or_not q \0c); first by move -> ; rewrite cprod0r; apply: cle0n. move => qz; move: (cpred_pr qN qz) =>[sa sb]. case: (NleT_el (NS_prod bN qN) aN) => //; rewrite {1} sb => W. by case: (cleNgt(qb _ sa W)); rewrite{2} sb; apply: cltS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)