fact: Fixpoint ins x vx s := match s with | Leaf => Rd Leaf x vx Leaf | Node c l y vy r => match K.compare x y with | Eq => Node c l y vx r | Lt => match c with | Red => Rd (ins x vx l) y vy r | Black => lbal (ins x vx l) y vy r end | Gt => match c with | Red => Rd l y vy (ins x vx r) | Black => rbal l y vy (ins x vx r) end end end.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)