proposition: Lemma rb_maxdepth s n : rbt n s -> maxdepth s <= 2*n + redcarac s.
proof: Proof. induction 1. - simpl; auto. - replace (redcarac l) with 0 in * by now destree l. replace (redcarac r) with 0 in * by now destree r. simpl maxdepth. simpl redcarac. rewrite Nat.add_succ_r, <- Nat.succ_le_mono. now apply Nat.max_lub. - simpl. rewrite <- Nat.succ_le_mono. apply Nat.max_lub; eapply Nat.le_trans; eauto; [destree l | destree r]; simpl; rewrite !Nat.add_0_r, ?Nat.add_1_r, ?Nat.add_succ_r; auto. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat