proposition: Lemma join_bst : forall l x d r, bst l -> bst r -> lt_tree x l -> gt_tree x r -> bst (join l x d r).
proof: Proof. join_tac; auto; try (simpl; auto; fail); inv bst; apply bal_bst; auto; clear Hrl Hlr; intro; intros; rewrite join_in in *. - intuition; [ apply MX.lt_eq with x | ]; eauto with ordered_type. - intuition; [ apply MX.eq_lt with x | ]; eauto with ordered_type. Qed.
imports: FunInd FMapInterface FMapList ZArith Int