Quotient and offset 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.

Comparing x - c with a boundary is comparing x with the boundary plus c. The Minus1 functions use this to compare an unrounded value with shifted boundaries, so the subtraction is never rounded on its own.

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.

theorem FloatLib.Numerics.cmp_sub_eq_cmp_add {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (x c b : α) : cmp (x - c) b = cmp x (b + c)

Subtracting a constant from the compared value adds it to the boundary.