a b c : ℚ
this : Rat.Nonneg (b - a) ∨ Rat.Nonneg (-(b - a))
⊢ a ≤ b ∨ b ≤ a
a b c : ℚ
⊢ a ≤ b ∨ b ≤ a
have := Rat.nonneg_total (b - a)
a b c : ℚ
this : Rat.Nonneg (b - a) ∨ Rat.Nonneg (-(b - a))
⊢ Rat.Nonneg (b - a) ∨ Rat.Nonneg (a - b)
a b c : ℚ
this : Rat.Nonneg (b - a) ∨ Rat.Nonneg (-(b - a))
⊢ a ≤ b ∨ b ≤ a
rw [Rat.le_iff_Nonneg, Rat.le_iff_Nonneg]
no goals
a b c : ℚ
this : Rat.Nonneg (b - a) ∨ Rat.Nonneg (-(b - a))
⊢ Rat.Nonneg (b - a) ∨ Rat.Nonneg (a - b)
rwa [neg_sub] at this