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. + refine (Nat.le_trans _ _ _ _ IHrbt1). apply Nat.le_add_r. + refine (Nat.le_trans _ _ _ _ IHrbt2). apply Nat.le_add_r. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat