proposition: Lemma cdivides_sum a a' b: b %|c a -> b %|c a' -> (b %|c (a +c a') /\ (a +c a') %/c b = (a %/c b) +c (a' %/c b)).
proof: Proof. move=> d1 d2. move: (cdivides_pr d1)(cdivides_pr d2)=> am bm. set s := (a %/c b) +c (a' %/c b). have ->: (a +c a' = b *c s) by rewrite /s cprodDr -am -bm. move: d1 d2 => [aN bN _][a'N _ _]. have sN:natp s by rewrite /s; fprops. split; first by apply: cdivides_pr1 =>//. case: (equal_or_not b \0c) => bs. rewrite {2} /s bs ! cquo_zero csum0l; fprops. by symmetry; apply: (cdivides_pr2 (NS_prod bN sN) bN sN bs). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)