proposition: Lemma power_commute_with_x : forall x n , x * x ** n = x ** n * x.
proof: Proof. induction n;simpl;power_simpl;trivial. repeat rewrite <- (@dot_assoc A dot one M); rewrite IHn; trivial. Qed.
imports: ZArith Arith Mat Program