proposition: Lemma cdivides_diff a a' b: a' <=c a -> b %|c a -> b %|c a' -> [/\ b %|c (a -c a'), (a' %/c b) <=c (a %/c b) & (a -c a') %/c b = (a %/c b) -c (a' %/c b)].
proof: Proof. move=> le d1 d2. move: (cdivides_pr d1)(cdivides_pr d2)=> am bm. set s := (a %/c b) -c (a' %/c b). move: d1 d2 => [aN bN _][a'N _ _]. move: (NS_quo b aN)(NS_quo b a'N) => q1 q2. have q3: (a' %/c b) <=c (a %/c b). case: (equal_or_not b \0c) => bnz. rewrite bnz ! cquo_zero; fprops. rewrite am bm in le; apply: (cprod_le2l bN q2 q1 bnz le). have ->: (a -c a' = b *c s). by rewrite /s cprodBl // -am -bm. 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 cdiff_nn; fprops. by symmetry; apply: (cdivides_pr2 (NS_prod bN sN) bN sN bs). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)