locator (join x y). Proof. intros q r ltqr. destruct (l q r ltqr, m q r ltqr) as [[ltqx|ltxr] [ltqy|ltyr]]. - apply inl, join_lt_l_l; assumption. - apply inl, join_lt_l_l; assumption. - apply inl, join_lt_l_r; assumption. - apply inr, join_lt_r; assumption. Qed.
Require Import