locator (// (x ; recip_neg_nu)). Proof. assert (negxpos : 0 < (-x)) by (apply flip_neg_negate; assumption). assert (l' := locator_minus (locator_recip_pos (locator_minus l) negxpos)). rewrite (recip_negate (-x)) in l'. unfold negate_apart in l'. rewrite (recip_proper_alt (- - x) x (apart_negate (- x) (positive_apart_zero (- x) negxpos)) recip_neg_nu) in l'. - assumption. - apply negate_involutive. Qed.
Require Import