Lemmas about invOf in ordered (semi)rings.

@[simp]

theorem invOf_pos {R : Type u_1} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} [Invertible a] : 0 < ⅟ a ↔ 0 < a

@[simp]

theorem invOf_nonpos {R : Type u_1} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} [Invertible a] : ⅟ a ≤ 0 ↔ a ≤ 0

@[simp]

theorem invOf_nonneg {R : Type u_1} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} [Invertible a] : 0 ≤ ⅟ a ↔ 0 ≤ a

@[simp]

theorem invOf_lt_zero {R : Type u_1} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} [Invertible a] : ⅟ a < 0 ↔ a < 0

@[simp]

theorem invOf_le_one {R : Type u_1} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} [Invertible a] (h : 1 ≤ a) : ⅟ a ≤ 1

theorem pos_invOf_of_invertible_cast {R : Type u_1} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [Nontrivial R] (n : ℕ) [Invertible ↑n] : 0 < ⅟ ↑n