fact: Definition bal l x d r := let hl := height l in let hr := height r in if (hr+2) <? hl then match l with | Leaf _ => assert_false l x d r | Node _ ll lx ld lr => if (height lr) <=? (height ll) then create ll lx ld (create lr x d r) else match lr with | Leaf _ => assert_false l x d r | Node _ lrl lrx lrd lrr => create (create ll lx ld lrl) lrx lrd (create lrr x d r) end end else if (hl+2) <? hr then match r with | Leaf _ => assert_false l x d r | Node _ rl rx rd rr => if (height rl) <=? (height rr) then create (create l x d rl) rx rd rr else match rl with | Leaf _ => assert_false l x d r | Node _ rll rlx rld rlr => create (create l x d rll) rlx rld (create rlr rx rd rr) end end else create l x d r.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)