x y : 0 < x * y -> (0 < x /\ 0 < y) |_| (x < 0 /\ y < 0). Proof. intros. assert (0 ≶ x /\ apart 0 y) as [Ex Ey];[split|]. - apply (strong_extensionality (.* y)). rewrite mult_0_l. apply pseudo_order_lt_apart;trivial. - apply (strong_extensionality (x *.)). rewrite mult_0_r. apply pseudo_order_lt_apart;trivial. - apply apart_iff_total_lt in Ex;apply apart_iff_total_lt in Ey. destruct Ex as [Ex|Ex], Ey as [Ey|Ey]; try auto. + destruct (irreflexivity (<) 0). transitivity (x * y); [trivial |]. apply pos_neg_mult;trivial. + destruct (irreflexivity (<) 0). transitivity (x * y); [trivial |]. apply neg_pos_mult;trivial. Qed.
Require Import