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