proposition: Lemma bal_bst : forall l x e r, bst l -> bst r -> lt_tree x l -> gt_tree x r -> bst (bal l x e r).
proof: Proof. intros l x e r; functional induction (bal l x e r); intros; clearf; inv bst; repeat apply create_bst; auto; unfold create; try constructor; (apply lt_tree_node || apply gt_tree_node); auto with ordered_type; (eapply lt_tree_trans || eapply gt_tree_trans); eauto with ordered_type. Qed.
imports: FunInd FMapInterface FMapList ZArith Int