proposition: Lemma lt_tree_node : forall (x y : elt) (l r : tree) (i : Info.t), lt_tree x l -> lt_tree x r -> X.lt y x -> lt_tree x (Node i l y r).
proof: Proof. unfold lt_tree; intuition_in; order. Qed.
imports: Orders OrdersFacts MSetInterface PeanoNat