proposition: Lemma Z_pow_compat : forall x y: Z, Z_pow x y = (x ^ y)%Z.
proof: Proof. intros x y; unfold Z_pow, Z.pow. destruct y; [ | rewrite Z_pow_compat_pos | ]; reflexivity. Qed.
imports: additions(Monoid_def Monoid_instances Pow) Coq(Lia ArithRing)