proposition: Lemma remove_min_gt_tree : forall l x e r h, bst (Node l x e r h) -> gt_tree (remove_min l x e r)#2#1 (remove_min l x e r)#1.
proof: Proof. intros l x e r; functional induction (remove_min l x e r); simpl in *; intros. - inv bst; auto. - inversion_clear H. intro; intro. rewrite e0 in *;simpl in *. generalize (IHp _x H0). generalize (remove_min_in ll lx ld lr _x m#1). rewrite e0; simpl; intros. rewrite (bal_in l' x d r y) in H. assert (In m#1 (Node ll lx ld lr _x)) by (rewrite H4; auto with ordered_type); clear H4. assert (X.lt m#1 x) by order. decompose [or] H; order. Qed.
imports: FunInd FMapInterface FMapList ZArith Int