proposition: Lemma cdivides_pr1 a b: natp a -> natp b -> b %|c (b *c a).
proof: Proof. move=> aN bN. move: (NS_prod bN aN) => pN. split => //. case: (equal_or_not b \0c) => bnz. rewrite bnz cprod0l crem_zero //; fprops. by case: (cquorem_pr0 pN bN aN bnz (refl_equal (b *c a))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)