fact: Definition bal l x r := let hl := height l in let hr := height r in if (hr+2) <? hl then match l with | Leaf => assert_false l x r | Node _ ll lx lr => if (height lr) <=? (height ll) then create ll lx (create lr x r) else match lr with | Leaf => assert_false l x r | Node _ lrl lrx lrr => create (create ll lx lrl) lrx (create lrr x r) end end else if (hl+2) <? hr then match r with | Leaf => assert_false l x r | Node _ rl rx rr => if (height rl) <=? (height rr) then create (create l x rl) rx rr else match rl with | Leaf => assert_false l x r | Node _ rll rlx rlr => create (create l x rll) rlx (create rlr rx rr) end end else create l x r.
imports: FunInd MSetInterface MSetGenTree BinInt Int