locator (// (x ; nu)). Proof. destruct (fst (apart_iff_total_lt x 0) nu) as [xneg|xpos]. - set (l' := locator_recip_neg l xneg). rewrite (recip_proper_alt x x (negative_apart_zero x xneg) nu) in l'; try reflexivity; exact l'. - set (l' := locator_recip_pos l xpos). rewrite (recip_proper_alt x x (positive_apart_zero x xpos) nu) in l'; try reflexivity; exact l'. Qed.
Require Import