d : ℤ
hd : d ≤ 0
n : ℤ√d
⊢ 0 ≤ -d * (n.im * n.im)
d : ℤ
hd : d ≤ 0
n : ℤ√d
⊢ 0 ≤ -(d * n.im * n.im)
rw [mul_assoc, neg_mul_eq_neg_mul]
no goals
d : ℤ
hd : d ≤ 0
n : ℤ√d
⊢ 0 ≤ -d * (n.im * n.im)
exact mul_nonneg (neg_nonneg.2 hd) (mul_self_nonneg _)