proposition: Lemma maxdepth_upperbound elt (s:t elt) : Avl s -> maxdepth s <= 2 * Nat.log2 (cardinal s) + 1.
proof: Proof. intros. transitivity (2 * Nat.log2 (mincard (maxdepth s)) + 1). apply mincard_log. apply Nat.add_le_mono_r, Nat.mul_le_mono_l, Nat.log2_le_mono. now apply mincard_maxdepth. Qed.
imports: Coq(ZArith Int Lia PeanoNat FunInd Orders) MMaps(GenTree AVL)