-- -> {auto leftBoundOk  : (optional leftBounds  ((`LT` pivot) . Builtin.snd) Unit)}
        -- -> {auto rightBoundOk : (optional rightBounds ((`GT` pivot) . Builtin.fst) Unit)}

        -- -> {auto leftBoundOk  : (optional leftBounds  ((`LT` @{o} pivot) . Builtin.snd) Unit)}
        -- -> {auto rightBoundOk : (optional rightBounds ((`GT` @{o} pivot) . Builtin.fst) Unit)}

public export
Uninhabited (NonEmpty Empty {o}) where
  uninhabited IsNode impossible
data RotatableLeft : AVLTree t h b {o} -> Type where
  IsRotatableLeft : {leftTree : AVLTree t h1 b1 {o}} -> {rightTree : AVLTree t h2 b2 {o}}
                  -> {auto rightNonEmpty : NonEmpty rightTree}
                  -> {auto heightCheck : diff h1 h2 `LTE` 1}
                  -> RotatableLeft (Node leftTree _ rightTree {heightCheck=ok})
data RotatableRight : AVLTree t h b {o} -> Type where
  IsRotatableRight : {h1, h2 : Natural} -> {leftTree : AVLTree t h1 b1 {o}} -> {rightTree : AVLTree t h2 b2 {o}}
                   -> {auto leftNonEmpty : NonEmpty leftTree}
                   -> {auto heightCheck : diff h1 h2 `LTE` 1}
                   -> RotatableRight (Node leftTree _ rightTree {leftHeight=h1} {rightHeight=h2} {heightCheck=heightCheck})
rotateLeft : (tree : AVLTree t h b {o}) -> {auto ok: RotatableLeft tree} -> AVLTree t h' b' {o}
rotateLeft (Node treeA pivot1 Empty) {ok} = case ok of
  IsRotatableLeft {rightNonEmpty} => absurd rightNonEmpty
rotateLeft (Node treeA pivot1 (Node treeB pivot2 treeC)) {ok} = case ok of
  IsRotatableLeft {heightCheck} => ?holeRotateLeft
rotateRight : (tree : AVLTree t h b {o}) -> {auto ok: RotatableRight tree} -> AVLTree t h' b' {o}
rotateRight (Node Empty pivot2 treeB) {ok} = case ok of
  IsRotatableRight {leftNonEmpty} => absurd leftNonEmpty
rotateRight (Node (Node treeA pivot1 treeB) pivot2 treeC) {ok} = case ok of
  IsRotatableRight {heightCheck} => ?holeRotateRight