proposition: Lemma mindepth_cardinal s : 2^(mindepth s) <= S (cardinal s).
proof: Proof. unfold Peano.lt. induction s as [|c l IHl x r IHr]. - auto. - simpl. rewrite <- Nat.add_succ_r, <- Nat.add_succ_l, Nat.add_0_r. apply Nat.add_le_mono; etransitivity; try apply IHl; try apply IHr; apply Nat.pow_le_mono; auto. * apply Nat.le_min_l. * apply Nat.le_min_r. Qed.
imports: Orders OrdersFacts MSetInterface PeanoNat