proposition: Lemma N_pow_power : forall n a , (a ^ n )%N = power a (N.to_nat n).
proof: Proof. intros n a; unfold N.pow. destruct n as [ | p]. - compute; reflexivity. - simpl; destruct a. + assert (0 <> Pos.to_nat p)%nat. { generalize (Pos2Nat.is_pos p). intro;lia. } generalize H; clear H; generalize (Pos.to_nat p). intro n;induction n;simpl;auto. destruct 1;auto. + rewrite Pos_pow_power;now rewrite Npos_power_compat. Qed.
imports: additions(Monoid_def Monoid_instances Pow) Coq(Lia ArithRing)