proposition: Lemma power_of_square : forall x n, (x * x) ** n = x ** n * x ** n.
proof: Proof. induction n;simpl;monoid_simpl;trivial. repeat rewrite dot_assoc;rewrite IHn; repeat rewrite dot_assoc. factorize; simpl;trivial. Qed.
imports: ZArith Arith Mat Program