proposition: Lemma max_elt_spec2 s x y `{Ok s} : max_elt s = Some x -> InT y s -> ~ X.lt x y.
proof: Proof. revert x y; induction H as [|? z l r Hl IHl Hr IHr Hlt Hgt]; simpl in *; [discriminate|]. intros x y He Hi; apply In_node_iff in Hi. destruct r as [|t l1 w l2]. + intros; replace z with x in * by congruence. destruct Hi as [Hi|[Hi|Hi]]; try order. apply In_leaf_iff in Hi; contradiction. + destruct Hi as [Hi|[Hi|Hi]]. - intros H. apply max_elt_spec1, Hgt in He. elim (lt_tree_not_in y l); [|assumption]. eapply lt_tree_trans; [|exact Hlt]; order. - intros H; eapply gt_tree_trans in Hgt; [|rewrite <- Hi; eassumption]. apply max_elt_spec1 in He; apply gt_tree_not_in in Hgt; contradiction. - apply IHr; assumption. Qed.
imports: Orders OrdersFacts MSetInterface PeanoNat