proposition: Lemma eqmod_sum a b a' b': natp a -> natp b -> natp a' -> natp b' -> a = a' %c[mod B] -> b = b' %c[mod B] -> a +c b = a' +c b' %c[mod B].
proof: Proof. move=> aN bN a'N b'N e1 e2. rewrite (crem_sum aN bN) e1 e2 (crem_sum a'N b'N); reflexivity. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)