proposition: Lemma mincard_maxdepth elt (s:t elt) : Avl s -> mincard (maxdepth s) <= cardinal s.
proof: Proof. induction 1. - simpl; auto. - simpl maxdepth. simpl cardinal. subst h. destruct (Nat.max_spec (maxdepth l) (maxdepth r)) as [(U,->)|(U,->)]. * rewrite mincard_bound. apply -> Nat.succ_le_mono. apply Nat.add_le_mono; eauto. apply Nat2Z.inj_le. rewrite Nat2Z.inj_add. rewrite 2 maxdepth_heigth by auto. simpl Z.of_nat. i2z. lia. * rewrite Nat.add_comm, mincard_bound. apply -> Nat.succ_le_mono. apply Nat.add_le_mono; eauto. apply Nat2Z.inj_le. rewrite Nat2Z.inj_add. rewrite 2 maxdepth_heigth by auto. simpl Z.of_nat. i2z. lia. Qed.
imports: Coq(ZArith Int Lia PeanoNat FunInd Orders) MMaps(GenTree AVL)