proposition: Lemma ins_rr_rb x e s n : rbt n s -> ifred s (rrt n (ins x e s)) (rbt n (ins x e s)).
proof: Proof. induction 1 as [ | n l k v r | n l k v r Hl IHl Hr IHr ]. - simpl; autom. - simpl. rewrite ifred_notred in * by trivial. destmatch; autom. - rewrite ifred_notred by autom. cbn. destmatch; intro. * autom. * apply lbal_rb; trivial. apply ifred_or in IHl; intuition (auto with map). * apply rbal_rb; trivial. apply ifred_or in IHr; intuition (auto with map). Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList Arith) Coq(Orders OrdersFacts OrdersLists) MMaps(Interface GenTree RBT)