proposition: Lemma crem_sum a b: natp a -> natp b -> a +c b = a %%c B +c b %%c B %c[mod B].
proof: Proof. move=> aN bN. move: (cdivision aN BN Bnz) (cdivision bN BN Bnz). set q1:= a %/c B; set q2:= b %/c B; set r1:= a %%c B; set r2:= b %%c B. move=> [q1N r1N [aeq r1p]][q2N r2N [beq r2p]]. rewrite aeq beq csumACA - cprodDr; apply: crem_prop; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)