proposition: Lemma min_elt_spec2 s x y `{Ok s} : min_elt s = Some x -> InT y s -> ~ X.lt y x.
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 l 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]]. - apply IHl; assumption. - intros H; eapply lt_tree_trans in Hlt; [|rewrite <- Hi; eassumption]. apply min_elt_spec1 in He; apply lt_tree_not_in in Hlt; contradiction. - intros H. apply min_elt_spec1, Hlt in He. elim (gt_tree_not_in y r); [|assumption]. eapply gt_tree_trans; [|exact Hgt]; order. Qed.
imports: Orders OrdersFacts MSetInterface PeanoNat