proposition: Lemma add_avl_1 : forall s x e `{!Avl s}, Avl (add x e s) /\ 0 <= height (add x e s) - height s <= 1.
proof: Proof. induct s; inv_avl. - intuition; try constructor; simpl; autom; lia_max. - simpl. intuition (auto with map typeclass_instances); lia_max. - destruct (IHl x e); trivial. split. * apply bal_avl; trivial; lia_max. * lia_bal. - destruct (IHr x e); trivial. split. * apply bal_avl; trivial; lia_max. * lia_bal. Qed.
imports: Coq(ZArith Int Lia PeanoNat FunInd Orders) MMaps(GenTree AVL)