proposition: Lemma eqmod_pow1 a n: natp a -> natp n -> a = \1c %c[mod B] -> a ^c n = \1c %c[mod B].
proof: Proof. move=> aN nN h; move: n nN. apply: Nat_induction; first by rewrite cpowx0. move=> n nN h1. move: (eqmod_prod (NS_pow aN nN) aN NS1 NS1 h1 h). rewrite (cpow_succ _ nN) (cprod1r); fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)