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