proposition: Lemma cdiff_pr4 a b a' b': natp a -> natp b -> natp a' -> natp b' -> a <=c b -> a' <=c b' -> (b +c b') -c (a +c a') = (b -c a) +c (b' -c a').
proof: Proof. move=> aN bN a'N b'N ab a'b'. have aux: ((b -c a) +c b') +c a = b' +c b. by rewrite (csumC _ b') - csumA cdiff_rpr. apply: cdiff_pr2; fprops. by rewrite (csumC a a') csumA - (csumA _ _ a') (cdiff_rpr a'b') aux csumC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)