proposition: Lemma mindepth_maxdepth m : mindepth m <= maxdepth m.
proof: Proof. induction m; simpl; auto. rewrite <- Nat.succ_le_mono. transitivity (mindepth m1). apply Nat.le_min_l. transitivity (maxdepth m1). trivial. apply Nat.le_max_l. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)