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; auto. - split; auto. - intros n. invrb. case (IHlr n); auto; clear IHlr. case append_rr_match. + intros a x b _ H; split; invrb. assert (rbt n (Rd a x b)) by auto. invrb. auto. + split; invrb; auto. - split; invrb. destruct (IHlr n) as (_,IH); auto. - split; invrb. destruct (IHrl n) as (_,IH); auto. - nonzero n. invrb. destruct (IHlr n) as (IH,_); auto; clear IHlr. revert IH. case append_bb_match. + intros a x b IH; split; destruct IH; invrb; auto. + split; [left | invrb]; auto using lbalS_rb. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat