proposition: Theorem power_of_mult : forall n x y, power (dot x y) n = dot (power x n) (power y n).
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 Arith Mat Program