[STATEMENT]
lemma of_complex_mult [simp]: "of_complex (x * y) = of_complex x * of_complex y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex (x * y) = of_complex x * of_complex y
[PROOF STEP]
by (simp add: of_complex_def mult.commute)