(x : F) (Px : x < 0) : //(x;negative_apart_zero x Px) < 0. 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.
Require Import