proposition: Lemma eqmod_succ a a': natp a -> natp a' -> a = a' %c[mod B] -> csucc a = csucc a' %c[mod B].
proof: Proof. move=> aN a'N e1. rewrite !csucc_pr4; fprops; apply: eqmod_sum => //; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)