proposition: Lemma maxdepth_log_cardinal s : s <> Leaf -> Nat.log2 (cardinal s) < maxdepth s.
proof: Proof. intros H. apply Nat.log2_lt_pow2. - destruct s; simpl; intuition auto with arith. - apply maxdepth_cardinal. Qed.
imports: Orders OrdersFacts MSetInterface PeanoNat