proposition: Lemma remove_avl_1 : forall s x `{!Avl s}, Avl (remove x s) /\ 0 <= height s - height (remove x s) <= 1.
proof: Proof. induct s; inv_avl. - intuition (auto with map typeclass_instances); lia_max. - generalize (@append_avl_1 l r). intuition lia_max. - destruct (IHl x); trivial. split. * apply bal_avl; trivial; lia_max. * lia_bal. - destruct (IHr x); trivial. split. * apply bal_avl; trivial; lia_max. * lia_bal. Qed.
imports: Coq(ZArith Int Lia PeanoNat FunInd Orders) MMaps(GenTree AVL)