proposition: Lemma mindepth_maxdepth s : mindepth s <= maxdepth s.
proof: Proof. induction s; simpl; auto. rewrite <- Nat.succ_le_mono. transitivity (mindepth s1). - apply Nat.le_min_l. - transitivity (maxdepth s1). + trivial. + apply Nat.le_max_l. Qed.
imports: Orders OrdersFacts MSetInterface PeanoNat