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