proposition: Lemma neg_recip_compat (x : F) (Px : x < 0) : //(x;negative_apart_zero x Px) < 0.
proof: Proof. set (negxpos := fst (flip_neg_negate x) Px). apply (strictly_order_reflecting ((-x) *.)). rewrite mult_0_r. rewrite <- negate_mult_distr_l. rewrite (recip_inverse' x). apply flip_pos_negate, lt_0_1. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.fields HoTT.Classes.orders.rings