proposition: Lemma cdivides_trans1 a b a': a %|c a' -> b %|c a -> a' %/c b = (a' %/c a) *c (a %/c b).
proof: Proof. move=> d1 d2. move: (cdivides_pr d1). rewrite {1} (cdivides_pr d2) - cprodA => h. case: (equal_or_not b \0c) => bnz. by rewrite bnz cquo_zero cquo_zero cprod0r. move: d1 d2 => [a'N aN _][_ bN _]. have pN: natp ((a %/c b) *c (a' %/c a)) by fprops. rewrite - (cdivides_pr2 a'N bN pN bnz h). by rewrite cprodC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)