proposition: Lemma crem_succ a B: natp a -> natp B -> \1c <c B -> csucc a = csucc (a %%c B) %c[mod B].
proof: Proof. move => aN BN Bp. have Bnz: B <> \0c by move => h; apply:(@clt0 \1c); rewrite - h. move:(crem_sum BN Bnz aN NS1). by rewrite - (crem_small BN Bp) - (Nsucc_rw aN) - (Nsucc_rw (NS_rem B aN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)