proposition: Lemma remove_min_find : forall l x e r h y, bst (Node l x e r h) -> find y (Node l x e r h) = match X.compare y (remove_min l x e r)#2#1 with | LT _ => None | EQ _ => Some (remove_min l x e r)#2#2 | GT _ => find y (remove_min l x e r)#1 end.
proof: Proof. intros. destruct X.compare. - rewrite not_find_iff; auto. rewrite remove_min_in; red; destruct 1 as [H'|H']; [ order | ]. generalize (remove_min_gt_tree H H'); order. - apply find_1; auto. rewrite remove_min_mapsto; auto. - rewrite find_mapsto_equiv; eauto; intros. rewrite remove_min_mapsto; intuition; order. Qed.
imports: FunInd FMapInterface FMapList ZArith Int