proposition: Lemma remove_min_avl_1 : forall l x e r h, avl (Node l x e r h) -> avl (remove_min l x e r)#1 /\ 0 <= height (Node l x e r h) - height (remove_min l x e r)#1 <= 1.
proof: Proof. intros l x e r; functional induction (remove_min l x e r); simpl in *; intros. - inv avl; simpl in *; split; auto. avl_nns; omega_max. - inversion_clear H. rewrite e0 in IHp;simpl in IHp;destruct (IHp _x); auto. split; simpl in *. + apply bal_avl; auto; omega_max. + omega_bal. Qed.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia