no goals
R : Type ?u.89486
S : Type ?u.89489
a b : ℂ
r : ℝ
hab : a < b
hr : 0 < r
⊢ (r • a).re ≤ (r • b).re
simp [hr, hab.1.le]
no goals
R : Type ?u.89486
S : Type ?u.89489
a b : ℂ
r : ℝ
hab : a < b
hr : 0 < r
⊢ (r • a).im = (r • b).im
simp [hab.2]