proposition: Lemma maxdepth_log_cardinal m : m <> Leaf _ -> Nat.log2 (cardinal m) < maxdepth m.
proof: Proof. intros H. apply Nat.log2_lt_pow2. destruct m; simpl; intuition (auto with map arith). apply maxdepth_cardinal. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)