d : ℕ
a : ℤ√↑d
ha✝ : Nonneg a
x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
⊢ Nonneg { re := -(↑d * ↑y), im := ↑x }
d : ℕ
a : ℤ√↑d
ha✝ : Nonneg a
x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
⊢ Nonneg (sqrtd * { re := ↑x, im := -↑y })
simp only [muld_val, mul_neg]
d : ℕ
a : ℤ√↑d
ha✝ : Nonneg a
x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
⊢ SqLe (d * y) 1 x d
d : ℕ
a : ℤ√↑d
ha✝ : Nonneg a
x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
⊢ Nonneg { re := -(↑d * ↑y), im := ↑x }
apply nonnegg_neg_pos.2
no goals
d : ℕ
a : ℤ√↑d
ha✝ : Nonneg a
x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
⊢ SqLe (d * y) 1 x d
simpa [SqLe, mul_comm, mul_left_comm] using Nat.mul_le_mul_left d (nonnegg_pos_neg.1 ha)
d : ℕ
a : ℤ√↑d
ha✝ : Nonneg a
x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
⊢ Nonneg { re := ↑d * ↑y, im := -↑x }
d : ℕ
a : ℤ√↑d
ha✝ : Nonneg a
x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
⊢ Nonneg (sqrtd * { re := -↑x, im := ↑y })
simp only [muld_val]
d : ℕ
a : ℤ√↑d
ha✝ : Nonneg a
x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
⊢ SqLe x d (d * y) 1
d : ℕ
a : ℤ√↑d
ha✝ : Nonneg a
x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
⊢ Nonneg { re := ↑d * ↑y, im := -↑x }
apply nonnegg_pos_neg.2
no goals
d : ℕ
a : ℤ√↑d
ha✝ : Nonneg a
x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
⊢ SqLe x d (d * y) 1
simpa [SqLe, mul_comm, mul_left_comm] using Nat.mul_le_mul_left d (nonnegg_neg_pos.1 ha)