a✝ b✝ c✝ a b c : ℚ
hab : Rat.Nonneg (b - a)
hbc : Rat.Nonneg (c - b)
⊢ a ≤ c
a✝ b✝ c✝ a b c : ℚ
hab : a ≤ b
hbc : b ≤ c
⊢ a ≤ c
rw [Rat.le_iff_Nonneg] at hab hbc
a✝ b✝ c✝ a b c : ℚ
hab : Rat.Nonneg (b - a)
hbc : Rat.Nonneg (c - b)
this : Rat.Nonneg (b - a + (c - b))
⊢ a ≤ c
a✝ b✝ c✝ a b c : ℚ
hab : Rat.Nonneg (b - a)
hbc : Rat.Nonneg (c - b)
⊢ a ≤ c
have : Rat.Nonneg (b - a + (c - b)) := Rat.nonneg_add hab hbc
a✝ b✝ c✝ a b c : ℚ
hab : Rat.Nonneg (b - a)
hbc : Rat.Nonneg (c - b)
this : Rat.Nonneg (c - a)
⊢ a ≤ c
a✝ b✝ c✝ a b c : ℚ
hab : Rat.Nonneg (b - a)
hbc : Rat.Nonneg (c - b)
this : Rat.Nonneg (b - a + (c - b))
⊢ a ≤ c
simp_rw [sub_eq_add_neg, add_left_comm (b + -a) c (-b), add_comm (b + -a) (-b),
  add_left_comm (-b) b (-a), add_comm (-b) (-a), add_neg_cancel_comm_assoc,
  ← sub_eq_add_neg] at this
a✝ b✝ c✝ a b c : ℚ
hab : Rat.Nonneg (b - a)
hbc : Rat.Nonneg (c - b)
this : Rat.Nonneg (c - a)
⊢ Rat.Nonneg (c - a)
a✝ b✝ c✝ a b c : ℚ
hab : Rat.Nonneg (b - a)
hbc : Rat.Nonneg (c - b)
this : Rat.Nonneg (c - a)
⊢ a ≤ c
rw [Rat.le_iff_Nonneg]
no goals
a✝ b✝ c✝ a b c : ℚ
hab : Rat.Nonneg (b - a)
hbc : Rat.Nonneg (c - b)
this : Rat.Nonneg (c - a)
⊢ Rat.Nonneg (c - a)
exact this