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

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

case inr.inr
ι : Type ?u.164600
α : Type u_1
β : Type ?u.164606
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hb : 0 < b
⊢ 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b
ι : Type ?u.164600
α : Type u_1
β : Type ?u.164606
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
⊢ 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b
rcases lt_trichotomy b 0 with (hb | rfl | hb)
no goals
case inl
ι : Type ?u.164600
α : Type u_1
β : Type ?u.164606
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hb : b < 0
⊢ 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b
simp [hb, hb.not_lt, one_le_div_of_neg]
no goals
case inr.inl
ι : Type ?u.164600
α : Type u_1
β : Type ?u.164606
inst✝ : LinearOrderedField α
a c d : α
n : ℤ
⊢ 1 ≤ a / 0 ↔ 0 < 0 ∧ 0 ≤ a ∨ 0 < 0 ∧ a ≤ 0
simp [lt_irrefl, zero_lt_one.not_le, zero_lt_one]
no goals
case inr.inr
ι : Type ?u.164600
α : Type u_1
β : Type ?u.164606
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hb : 0 < b
⊢ 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b
simp [hb, hb.not_lt, one_le_div]