proposition: Lemma pos_mult_decompose x y : 0 < x * y → (0 < x ∧ 0 < y) ∨ (x < 0 ∧ y < 0).
proof: Proof. intros. assert (0 ≶ x) as Ex. apply (strong_extensionality (.* y)). rewrite mult_0_l. now apply pseudo_order_lt_apart. assert (0 ≶ y) as Ey. apply (strong_extensionality (x *.)). rewrite mult_0_r. now apply pseudo_order_lt_apart. 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_neg_mult. destruct (irreflexivity (<) 0). transitivity (x * y); [easy |]. now apply neg_pos_mult. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings MathClasses.orders.orders MathClasses.orders.maps