Quotient comparisons in ordered fields

Comparing a quotient with a boundary is equivalent to testing a linear residual against zero. A negative denominator reverses the ordering. These identities let interval-based comparisons use subtraction and multiplication without constructing quotient intervals.

theorem FloatLib.Numerics.cmp_div_of_pos {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (s c b : α) (hc : 0 < c) : cmp (s - b * c) 0 = cmp (s / c) b

A positive denominator preserves the ordering of the quotient's linear residual.

theorem FloatLib.Numerics.cmp_div_of_neg {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (s c b : α) (hc : c < 0) : (cmp (s - b * c) 0).swap = cmp (s / c) b

A negative denominator reverses the ordering of the quotient's linear residual.