proposition: Lemma cquorem_pr0 a b q: natp a -> natp b -> natp q -> b <> \0c -> a = (b *c q) -> (q = a %/c b /\ \0c = a %%c b).
proof: Proof. move => aN bN qN bnz p'. apply: cquorem_pr; fprops. hnf; rewrite -p' (Nsum0r aN). split; [ trivial | split; [ apply: cle0x | ]]; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)