proposition: Lemma maxdepth_upperbound s : Rbt s -> maxdepth s <= 2 * Nat.log2 (S (cardinal s)).
proof: Proof. intros (n,H). eapply Nat.le_trans; [eapply rb_maxdepth; eauto|]. transitivity (2*(n+redcarac s)). - rewrite Nat.mul_add_distr_l. apply Nat.add_le_mono_l. rewrite <- Nat.mul_1_l at 1. apply Nat.mul_le_mono_r. auto. - apply Nat.mul_le_mono_l. transitivity (mindepth s). + now apply rb_mindepth. + apply mindepth_log_cardinal. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat