[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedSemiring α
a : α
inst✝ : Invertible a
⊢ 0 < a * ⅟a
[PROOFSTEP]
simp only [mul_invOf_self, zero_lt_one]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedSemiring α
a : α
inst✝ : Invertible a
⊢ ⅟a ≤ 0 ↔ a ≤ 0
[PROOFSTEP]
simp only [← not_lt, invOf_pos]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedSemiring α
a : α
inst✝ : Invertible a
⊢ 0 < a * ⅟a
[PROOFSTEP]
simp only [mul_invOf_self, zero_lt_one]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedSemiring α
a : α
inst✝ : Invertible a
⊢ ⅟a < 0 ↔ a < 0
[PROOFSTEP]
simp only [← not_le, invOf_nonneg]
