no goals
ι : Type ?u.34425
α : Type u_1
β : Type ?u.34431
inst✝ : LinearOrderedSemifield α
a✝ b c d e : α
m n : ℤ
a : α
h : a = 0
⊢ a / a ≤ 1
simp [h]
no goals
ι : Type ?u.34425
α : Type u_1
β : Type ?u.34431
inst✝ : LinearOrderedSemifield α
a✝ b c d e : α
m n : ℤ
a : α
h : ¬a = 0
⊢ a / a ≤ 1
simp [h]