a✝ b✝ c a b : ℚ
hab : Rat.Nonneg (b - a)
hba : Rat.Nonneg (a - b)
⊢ a = b
a✝ b✝ c a b : ℚ
hab : a ≤ b
hba : b ≤ a
⊢ a = b
rw [Rat.le_iff_Nonneg] at hab hba
a✝ b✝ c a b : ℚ
hab : Rat.Nonneg (b - a)
hba : Rat.Nonneg (a + -b)
⊢ a = b
a✝ b✝ c a b : ℚ
hab : Rat.Nonneg (b - a)
hba : Rat.Nonneg (a - b)
⊢ a = b
rw [sub_eq_add_neg] at hba
a✝ b✝ c a b : ℚ
hab : Rat.Nonneg (-(a + -b))
hba : Rat.Nonneg (a + -b)
⊢ a = b
a✝ b✝ c a b : ℚ
hab : Rat.Nonneg (b - a)
hba : Rat.Nonneg (a + -b)
⊢ a = b
rw [←neg_sub, sub_eq_add_neg] at hab
a✝ b✝ c a b : ℚ
hab : Rat.Nonneg (-(a + -b))
hba : Rat.Nonneg (a + -b)
this : a = - -b
⊢ a = b
a✝ b✝ c a b : ℚ
hab : Rat.Nonneg (-(a + -b))
hba : Rat.Nonneg (a + -b)
⊢ a = b
have := eq_neg_of_add_eq_zero_left (Rat.nonneg_antisymm hba hab)
no goals
a✝ b✝ c a b : ℚ
hab : Rat.Nonneg (-(a + -b))
hba : Rat.Nonneg (a + -b)
this : a = - -b
⊢ a = b
rwa [neg_neg] at this