proposition: Lemma crem_prod 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 cprodDr (cprodC B q2) cprodA (cprodC _ B). rewrite (cprodDl r2) - cprodA csumA - cprodDr - aeq. by apply: crem_prop ; [apply: NS_sum | ]; apply: NS_prod. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)