proposition: Lemma crem_prop a b: natp a -> natp b -> B *c a +c b = b %c[mod B].
proof: Proof. move=> aN bN. move: (cdivision bN BN Bnz). set q := b %/c B; set r := b %%c B. move=> [q1N r1N [aeq r1p]]. rewrite aeq csumA - cprodDr. set q2:= (a +c q). have q2N: natp q2 by apply: NS_sum. have dp: (cdivision_prop ((B *c q2) +c r) B q2 r) by split. by move: (cquorem_pr (NS_sum (NS_prod BN q2N) r1N) BN q2N r1N dp) => [_]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)