proposition: Lemma concat_find : forall m1 m2 y, bst m1 -> bst m2 -> (forall y1 y2, In y1 m1 -> In y2 m2 -> X.lt y1 y2) -> find y (concat m1 m2) = match find y m2 with Some d => Some d | None => find y m1 end.
proof: Proof. intros m1 m2; functional induction (concat m1 m2); intros; auto; try factornode _x _x0 _x1 _x2 _x3 as m1. - simpl; destruct (find y m2); auto. - generalize (remove_min_find y H0)(remove_min_in l2 x2 d2 r2 _x4) (remove_min_bst H0)(remove_min_gt_tree H0); rewrite e1; simpl fst; simpl snd; intros. inv bst. rewrite H2, join_find; auto; clear H2. + simpl; destruct X.compare as [Hlt| |Hlt]; simpl; auto. destruct (find y m2'); auto. symmetry; rewrite not_find_iff; auto; intro. apply (MX.lt_not_gt Hlt); apply H1; auto; rewrite H3; auto with ordered_type. + intros z Hz; apply H1; auto; rewrite H3; auto with ordered_type. Qed.
imports: FunInd FMapInterface FMapList ZArith Int