fact: Definition rbalS l k vk r := match r with | Rd b y vy c => Rd l k vk (Bk b y vy c) | _ => match l with | Bk a x vx b => lbal (Rd a x vx b) k vk r | Rd a x vx (Bk b y vy c) => Rd (lbal (makeRed a) x vx b) y vy (Bk c k vk r) | _ => Rd l k vk r end end.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)