proposition: Lemma nltxr_locates_right {q r : Q} (l' : locator' x) (ltqr : q < r) : ~ (x < ' r) -> locates_right l' ltqr.
proof: Proof. intros nltxr. apply stable. assert (f := locates_right_false l' ltqr). exact (not_contrapositive f nltxr). Qed.
imports: HoTT.Basics HoTT.DProp HoTT.BoundedSearch HoTT.Spaces.Finite.Fin HoTT.ExcludedMiddle HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.interfaces.rationals HoTT.Classes.interfaces.cauchy HoTT.Classes.interfaces.archimedean HoTT.Classes.interfaces.round HoTT.Classes.interfaces.naturals HoTT.Classes.implementations.peano_naturals HoTT.Classes.orders.archimedean HoTT.Classes.orders.dec_fields HoTT.Classes.orders.lattices HoTT.Classes.theory.apartness HoTT.Classes.theory.rationals HoTT.Classes.orders.fields HoTT.Classes.theory.fields HoTT.Classes.theory.dec_fields