proposition: Lemma remove_min_bst : forall l x e r h, bst (Node l x e r h) -> bst (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; inversion_clear H0. apply bal_bst; auto. + rewrite e0 in *; simpl in *; apply (IHp _x); auto. + intro; intros. generalize (remove_min_in ll lx ld lr _x y). rewrite e0; simpl in *. destruct 1. apply H2; intuition. Qed.
imports: FunInd FMapInterface FMapList ZArith Int