Real semantics of reciprocal comparisons

On each half-line, inversion is strictly decreasing, so comparing t⁻¹ with a boundary b of the same sign is comparing b⁻¹ with t. Boundaries of the other sign are decided by the sign of t.

theorem FloatLib.Numerics.compareReciprocal_eq_real (compare : ℚ → Ordering) (t : ℝ) (ht : t ≠ 0) (hcompare : ∀ (q : ℚ), compare q = cmp t ↑q) (boundary : ℚ) : compareReciprocal compare boundary = cmp t⁻¹ ↑boundary

Given an exact comparator for a nonzero real t, compareReciprocal compares t⁻¹.