{q r : Q} (l' : locator' x) (ltqr : q < r) : ~ (x < ' r) -> locates_right l' ltqr. Proof. intros nltxr. apply stable. assert (f := locates_right_false l' ltqr). exact (not_contrapositive f nltxr). Qed.
Require Import