proposition: Lemma neg_mult_decompose x y : x * y < 0 → (x < 0 ∧ 0 < y) ∨ (0 < x ∧ y < 0).
proof: Proof. intros. assert (0 ≶ x) as Ex. apply (strong_extensionality (.* y)). rewrite mult_0_l. now apply pseudo_order_lt_apart_flip. assert (0 ≶ y) as Ey. apply (strong_extensionality (x *.)). rewrite mult_0_r. now apply pseudo_order_lt_apart_flip. rewrite apart_iff_total_lt in Ex, Ey. destruct Ex as [Ex|Ex], Ey as [Ey|Ey]; try tauto. destruct (irreflexivity (<) 0). transitivity (x * y); [| easy]. now apply pos_mult_compat. destruct (irreflexivity (<) 0). transitivity (x * y); [| easy]. now apply neg_mult. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings MathClasses.orders.orders MathClasses.orders.maps