proposition: Lemma power_x_plus : forall x n p, (x ** (n + p) = x ** n * x ** p).
proof: Proof. induction n;simpl. - intros; monoid_simpl;trivial. - intro p;rewrite (IHn p); monoid_simpl;trivial. Qed.
imports: ZArith Recdef Mat Ring