locator (-x). Proof. intros q r ltqr. assert (ltnrnq := snd (flip_lt_negate q r) ltqr : -r < -q). destruct (l _ _ ltnrnq) as [ltnrx|ltxnq]. - apply inr. apply char_minus_left. rewrite <- preserves_negate. assumption. - apply inl. apply char_minus_right. rewrite <- preserves_negate. assumption. Qed.
Require Import