proposition: Lemma Epower_x_mult `(M: EMonoid) : forall x n p, (Epower x (n * p)) == Epower (Epower x p) n.
proof: Proof. induction n;simpl. - reflexivity. - intro p; rewrite Epower_x_plus; now rewrite IHn. Qed.
imports: ZArith Recdef Mat Ring Coq.Setoids.Setoid Morphisms