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;[|assert (apart 0 y) as Ey]. - apply (strong_extensionality (.* y)). rewrite mult_0_l. apply pseudo_order_lt_apart_flip;trivial. - apply (strong_extensionality (x *.)). rewrite mult_0_r. apply pseudo_order_lt_apart_flip;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_mult_compat;trivial. + destruct (irreflexivity (<) 0). transitivity (x * y); [| trivial]. apply neg_mult;trivial. Qed.
imports: HoTT.Classes.theory.apartness HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.rings HoTT.Classes.orders.orders HoTT.Classes.orders.maps