proposition: Lemma concat_bst : forall m1 m2, bst m1 -> bst m2 -> (forall y1 y2, In y1 m1 -> In y2 m2 -> X.lt y1 y2) -> bst (concat m1 m2).
proof: Proof. intros m1 m2; functional induction (concat m1 m2); intros; auto; try factornode _x _x0 _x1 _x2 _x3 as m1. apply join_bst; auto. - change (bst (m2',xd)#1). rewrite <-e1; eauto. - intros y Hy. apply H1; auto. rewrite remove_min_in, e1; simpl; auto with ordered_type. - change (gt_tree (m2',xd)#2#1 (m2',xd)#1). rewrite <-e1; eauto. Qed.
imports: FunInd FMapInterface FMapList ZArith Int