locator (' s). Proof. intros q r ltqr. destruct (trichotomy _ s r) as [ltsr|[eqsr|ltrs]]. - apply inr, (strictly_order_preserving _); assumption. - rewrite <- eqsr in ltqr. apply inl, (strictly_order_preserving _); assumption. - apply inl, (strictly_order_preserving _), (transitivity ltqr ltrs). Qed.
Require Import