proposition: Lemma square_mult : forall n m, square (n * m) = square n * square m.
proof: Proof. intros n m. simpl. unfold square. rewrite mult_assoc. assert (H : n * m * n = n * n * m). { rewrite mul_comm. apply mult_assoc. } rewrite H. rewrite mult_assoc. reflexivity. Qed.