proposition: Lemma Pos_pow_compat : forall n (a:positive), (a ^ n )%positive = Pos_pow a n.
proof: Proof. unfold Pos_pow; intros;rewrite Pos_bpow_ok; now rewrite Pos_pow_power. Qed.
imports: additions(Monoid_def Monoid_instances Pow) Coq(Lia ArithRing)