proposition: Lemma Npos_power_compat : forall (n:nat)(a:positive), Npos (power a n) = power (Npos a) n.
proof: Proof. induction n. - now compute. - intros; repeat rewrite power_eq2; now rewrite <- IHn. Qed.
imports: additions(Monoid_def Monoid_instances Pow) Coq(Lia ArithRing)