proposition: Lemma rb_mindepth s n : rbt n s -> n + redcarac s <= mindepth s.
proof: Proof. induction 1; simpl. - trivial. - rewrite Nat.add_succ_r. apply -> Nat.succ_le_mono. replace (redcarac l) with 0 in * by now destree l. replace (redcarac r) with 0 in * by now destree r. now apply Nat.min_glb. - apply -> Nat.succ_le_mono. rewrite Nat.add_0_r. apply Nat.min_glb; eauto with arith. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList Arith) Coq(Orders OrdersFacts OrdersLists) MMaps(Interface GenTree RBT)