proposition: Lemma gt_tree_node : forall x y l r e h, gt_tree x l -> gt_tree x r -> X.lt x y -> gt_tree x (Node l y e r h).
proof: Proof. unfold gt_tree in *; intuition_in; order. Qed.
imports: FunInd FMapInterface FMapList ZArith Int