proposition: Lemma mindepth_log_cardinal m : mindepth m <= Nat.log2 (S (cardinal m)).
proof: Proof. apply Nat.log2_le_pow2. auto with arith. apply mindepth_cardinal. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)