proposition: Lemma remove_avl_1 : forall m x, avl m -> avl (remove x m) /\ 0 <= height m - height (remove x m) <= 1.
proof: Proof. intros m x; functional induction (remove x m); intros. - split; auto; omega_max. - inv avl. destruct (IHt H0). split. + apply bal_avl; auto. omega_max. + omega_bal. - inv avl. generalize (merge_avl_1 H0 H1 H2). intuition omega_max. - inv avl. destruct (IHt H1). split. + apply bal_avl; auto. omega_max. + omega_bal. Qed.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia