proposition: Lemma cdivides_pr4 b q: natp b -> natp q -> b <> \0c -> (b *c q) %/c b = q.
proof: Proof. move=> bN qN bnz; symmetry; apply: cdivides_pr2; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)