proposition: Lemma eqmod_pow2 a b n: natp a -> natp b -> natp n -> a = \1c %c[mod B] -> b *c a ^c n = b %c[mod B].
proof: Proof. move=> aN bN nN h. move: (eqmod_pow1 aN nN h) => h2. have aux: eqmod B b b by []. move: (eqmod_prod bN (NS_pow aN nN) bN NS1 aux h2). rewrite cprod1r; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)