proposition: Lemma del_arb s x n : rbt (S n) s -> isblack s -> arbt n (del x s) with del_rb s x n : rbt n s -> notblack s -> rbt n (del x s).
proof: Proof. { revert n. induct' s; descolor; try easy; invrb. - apply append_arb_rb; assumption. - assert (IHl' := del_rb l x). clear IHr del_arb del_rb. destruct l as [|[|] ll lx lv lr]; autom. nonzero n. apply lbalS_arb; autom. - assert (IHr' := del_rb r x). clear IHl del_arb del_rb. destruct r as [|[|] rl rx rv rr]; autom. nonzero n. apply rbalS_arb; auto. } { revert n. induct' s; descolor; try easy; invrb. - apply append_arb_rb; assumption. - assert (IHl' := del_arb l x). clear IHr del_arb del_rb. destruct l as [|[|] ll lx lv lr]; autom. nonzero n. destruct n as [|n]; [invrb|]; apply lbalS_rb; autom. - assert (IHr' := del_arb r x). clear IHl del_arb del_rb. destruct r as [|[|] rl rx rv rr]; autom. nonzero n. apply rbalS_rb; auto. } Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList Arith) Coq(Orders OrdersFacts OrdersLists) MMaps(Interface GenTree RBT)