no goals
ι : Type ?u.185600
α : Type u_1
β : Type ?u.185606
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
h : a < b
⊢ a + (b - a) / 2 < b
rwa [← div_sub_div_same, sub_eq_add_neg, add_comm (b / 2), ← add_assoc, ← sub_eq_add_neg, ←
  lt_sub_iff_add_lt, sub_self_div_two, sub_self_div_two, div_lt_div_right (zero_lt_two' α)]