proposition: Lemma power_x_plus : forall x n p, x ** (n + p) = x ** n * x ** p.
proof: Proof. induction n as [| p IHp];simpl. - intros; monoid_simpl;trivial. - intro q;rewrite (IHp q); monoid_simpl;trivial. Qed.
imports: ZArith Arith Mat Program