proposition: Lemma maxdepth_heigth elt (s:t elt) : Avl s -> Z.of_nat (maxdepth s) = i2z (height s).
proof: Proof. induction 1. simpl. lia_max. simpl maxdepth. simpl height. subst h. rewrite Nat2Z.inj_succ, Nat2Z.inj_max. lia_max. Qed.
imports: Coq(ZArith Int Lia PeanoNat FunInd Orders) MMaps(GenTree AVL)