[STATEMENT]
lemma star_of_Re [simp]: "star_of (Re x) = hRe (star_of x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hypreal_of_real (Re x) = hRe (hcomplex_of_complex x)
[PROOF STEP]
by transfer (rule refl)