theorem Rat.inv_lt_self_of_one_lt {x : ℚ} (h : 1 < x) : x⁻¹ < x

theorem Rat.inv_le_self_of_one_le {x : ℚ} (h : 1 ≤ x) : x⁻¹ ≤ x

theorem Rat.lt_inv_self_of {x : ℚ} (h₁ : 0 < x) (h₂ : x < 1) : x < x⁻¹

theorem Rat.le_inv_self_of {x : ℚ} (h₁ : 0 < x) (h₂ : x ≤ 1) : x ≤ x⁻¹