proposition: Lemma cquorem_pr a b q r: natp a -> natp b -> natp q -> natp r -> cdivision_prop a b q r -> (q = a %/c b /\ r = a %%c b).
proof: Proof. move => aN bN qN rN p'. case: (equal_or_not b \0c) => bnz. move: p' => [_ ]; rewrite bnz =>h; case: (clt0 h). move: (cdivision aN bN bnz)=> [qqN rrN p]. apply: (cdivision_unique aN bN qN rN qqN rrN bnz p' p). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)