proposition: Lemma Pos2Nat_morph : forall (n:nat)(a : positive), Pos.to_nat (a ^ n)%M = Pos.to_nat a ^ n.
proof: Proof. induction n. intro;simpl; reflexivity. intro; simpl. rewrite Pos2Nat.inj_mul. rewrite IHn. reflexivity. Qed.
imports: additions(Monoid_def Monoid_instances Pow) Coq(Lia ArithRing)