proposition: Lemma Pos_pow_power : forall n a : positive , (a ^ n )%positive = power a (Pos.to_nat n).
proof: Proof. intros n a; unfold Pos.pow. rewrite (Pos_iter_op_ok _ _ _ PMult). generalize (binary_power_mult_ok (E_one := xH) (E_eq := eq_equiv)). intro H; rewrite H. rewrite one_left. reflexivity. Qed.
imports: additions(Monoid_def Monoid_instances Pow) Coq(Lia ArithRing)