proposition: Lemma append_arb_rb n l r : rbt n l -> rbt n r -> (arbt n (append l r)) /\ (notred l -> notred r -> rbt n (append l r)).
proof: Proof. revert r n. append_tac l r. - split; autom. - split; autom. - intros n. invrb. case (IHlr n); auto; clear IHlr. case append_rr_match. + intros a x v b _ H; split; invrb. assert (rbt n (Rd a x v b)) by autom. invrb. autom. + split; invrb; autom. - split; invrb. destruct (IHlr n) as (_,IH); autom. - split; invrb. destruct (IHrl n) as (_,IH); autom. - nonzero n. invrb. destruct (IHlr n) as (IH,_); auto; clear IHlr. revert IH. case append_bb_match. + intros a x v b IH; split; destruct IH; invrb; autom. + split; [left | invrb]; auto using lbalS_rb with map. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList Arith) Coq(Orders OrdersFacts OrdersLists) MMaps(Interface GenTree RBT)