proposition: Lemma remove_min_avl_1 : forall l x e r h `{!Avl (Node h l x e r)}, Avl (remove_min l x e r)#1 /\ 0 <= height (Node h l x e r) - height (remove_min l x e r)#1 <= 1.
proof: Proof. intros l x e r; functional induction (remove_min l x e r); subst; simpl in *; intros. - inv_avl; simpl in *; split; auto. avl_nns; lia_max. - mysubst. inv_avl'; simpl in *. edestruct IHp; clear IHp; [eauto|]. split. * apply bal_avl; trivial; lia_max. * lia_bal. Qed.
imports: Coq(ZArith Int Lia PeanoNat FunInd Orders) MMaps(GenTree AVL)