d x y : ℕ
a : ℤ√↑d
ha : Nonneg a
this : { re := ↑x, im := ↑y } * a = ↑x * a + sqrtd * (↑y * a)
⊢ Nonneg ({ re := ↑x, im := ↑y } * a)
d x y : ℕ
a : ℤ√↑d
ha : Nonneg a
⊢ Nonneg ({ re := ↑x, im := ↑y } * a)
have : (⟨x, y⟩ * a : ℤ√d) = (x : ℤ√d) * a + sqrtd * ((y : ℤ√d) * a) := by
  rw [decompose, right_distrib, mul_assoc, Int.cast_ofNat, Int.cast_ofNat]
d x y : ℕ
a : ℤ√↑d
ha : Nonneg a
this : { re := ↑x, im := ↑y } * a = ↑x * a + sqrtd * (↑y * a)
⊢ Nonneg (↑x * a + sqrtd * (↑y * a))
d x y : ℕ
a : ℤ√↑d
ha : Nonneg a
this : { re := ↑x, im := ↑y } * a = ↑x * a + sqrtd * (↑y * a)
⊢ Nonneg ({ re := ↑x, im := ↑y } * a)
rw [this]
no goals
d x y : ℕ
a : ℤ√↑d
ha : Nonneg a
this : { re := ↑x, im := ↑y } * a = ↑x * a + sqrtd * (↑y * a)
⊢ Nonneg (↑x * a + sqrtd * (↑y * a))
exact (nonneg_smul ha).add (nonneg_muld <| nonneg_smul ha)
no goals
d x y : ℕ
a : ℤ√↑d
ha : Nonneg a
⊢ { re := ↑x, im := ↑y } * a = ↑x * a + sqrtd * (↑y * a)
rw [decompose, right_distrib, mul_assoc, Int.cast_ofNat, Int.cast_ofNat]