proposition: Lemma ins_rr_rb x s n : rbt n s -> ifred s (rrt n (ins x s)) (rbt n (ins x s)).
proof: Proof. induction 1 as [ | n l k r | n l k r Hl IHl Hr IHr ]. - simpl; auto. - simpl. rewrite ifred_notred in * by trivial. elim_compare x k; auto. - rewrite ifred_notred by trivial. unfold ins; fold ins. elim_compare x k. * auto. * apply lbal_rb; trivial. apply ifred_or in IHl; intuition. * apply rbal_rb; trivial. apply ifred_or in IHr; intuition. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat