d : ℕ
a b : ℤ√↑d
t : Nonneg (b - a) ∨ Nonneg (-(b - a))
⊢ a ≤ b ∨ b ≤ a
d : ℕ
a b : ℤ√↑d
⊢ a ≤ b ∨ b ≤ a
have t := (b - a).nonneg_total
no goals
d : ℕ
a b : ℤ√↑d
t : Nonneg (b - a) ∨ Nonneg (-(b - a))
⊢ a ≤ b ∨ b ≤ a
rwa [neg_sub] at t