fact: Fixpoint del x m : t := match m with | Leaf => Leaf | Node _ a y v b => match K.compare x y with | Eq => append a b | Lt => match a with | Bk _ _ _ _ => lbalS (del x a) y v b | _ => Rd (del x a) y v b end | Gt => match b with | Bk _ _ _ _ => rbalS a y v (del x b) | _ => Rd a y v (del x b) end end end.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)