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