proposition: Lemma cdivides_pr2 a b q: natp a -> natp b -> natp q -> b <> \0c -> a = b *c q -> q = a %/c b.
proof: Proof. move => aN bN qN nzb abq. by case: (cquorem_pr0 aN bN qN nzb abq). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)