proposition: Theorem power_of_mult : forall n x y, ((x * y) ** n = x ** n * y ** n)%M.
proof: Proof. induction n;simpl. - rewrite one_left;auto. - intros; rewrite IHn; repeat rewrite dot_assoc. rewrite <- (dot_assoc x y (power x n)); rewrite (dot_comm y (power x n)). repeat rewrite dot_assoc;trivial. Qed.
imports: ZArith Recdef Mat Ring