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