invOf_nonneg

theorem invOf_nonneg : ∀ {α : Type u_1} [inst : LinearOrderedSemiring α] {a : α} [inst_1 : Invertible a], 0 ≤ ⅟a ↔ 0 ≤ a

This theorem, `invOf_nonneg`, states that for any type `α` that is a linearly ordered semiring, and for any element `a` of `α` that is invertible, `a` is non-negative (i.e., `0 ≤ a`) if and only if its multiplicative inverse is also non-negative (i.e., `0 ≤ ⅟a`). This theorem demonstrates a fundamental property of numerical inverses in mathematical structures with an order and multiplication operation that satisfies the semiring axioms.

More concisely: For any linearly ordered semiring type `α` and invertible element `a` of `α`, `0 ≤ a` if and only if `0 ≤ ⅟a`.