ι : Type ?u.195915
α : Type u_1
β : Type ?u.195921
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
h : a < b
⊢ ∃ ε, ε > 0 ∧ a < b - ε
ι : Type ?u.195915
α : Type u_1
β : Type ?u.195921
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
h : ∀ (ε : α), ε > 0 → b - ε ≤ a
⊢ b ≤ a
contrapose! h
no goals
ι : Type ?u.195915
α : Type u_1
β : Type ?u.195921
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
h : a < b
⊢ ∃ ε, ε > 0 ∧ a < b - ε
simpa only [@and_comm ((0 : α) < _), lt_sub_iff_add_lt, gt_iff_lt] using
  exists_add_lt_and_pos_of_lt h