case inl
ι : Type ?u.170288
α : Type u_1
β : Type ?u.170294
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hb : b < 0
⊢ a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a

case inr.inl
ι : Type ?u.170288
α : Type u_1
β : Type ?u.170294
inst✝ : LinearOrderedField α
a c d : α
n : ℤ
⊢ a / 0 < 1 ↔ 0 < 0 ∧ a < 0 ∨ 0 = 0 ∨ 0 < 0 ∧ 0 < a

case inr.inr
ι : Type ?u.170288
α : Type u_1
β : Type ?u.170294
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hb : 0 < b
⊢ a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a
ι : Type ?u.170288
α : Type u_1
β : Type ?u.170294
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
⊢ a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a
rcases lt_trichotomy b 0 with (hb | rfl | hb)
no goals
case inl
ι : Type ?u.170288
α : Type u_1
β : Type ?u.170294
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hb : b < 0
⊢ a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a
simp [hb, hb.not_lt, hb.ne, div_lt_one_of_neg]
no goals
case inr.inl
ι : Type ?u.170288
α : Type u_1
β : Type ?u.170294
inst✝ : LinearOrderedField α
a c d : α
n : ℤ
⊢ a / 0 < 1 ↔ 0 < 0 ∧ a < 0 ∨ 0 = 0 ∨ 0 < 0 ∧ 0 < a
simp [zero_lt_one]
no goals
case inr.inr
ι : Type ?u.170288
α : Type u_1
β : Type ?u.170294
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hb : 0 < b
⊢ a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a
simp [hb, hb.not_lt, div_lt_one, hb.ne.symm]