Opposite signs

When two elements have opposite signs, and when two differences from a common point do: exactly when the point lies strictly between the two elements, or all three coincide.

Main results

• sign_eq_neg_sign_iff: two elements have opposite signs when they lie strictly on opposite sides of zero or both vanish.
• sign_sub_eq_neg_sign_sub_iff: a - c and b - c have opposite signs when c lies strictly between a and b, or a = b = c.

theorem sign_eq_neg_sign_iff {α : Type u_1} [Zero α] [LinearOrder α] {x y : α} : SignType.sign x = -SignType.sign y ↔ x < 0 ∧ 0 < y ∨ 0 < x ∧ y < 0 ∨ x = 0 ∧ y = 0

theorem sign_sub_eq_neg_sign_sub_iff {α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {a b c : α} : SignType.sign (a - c) = -SignType.sign (b - c) ↔ c ∈ Set.uIoo a b ∨ a = c ∧ b = c