meant to say a max bound of Nothing.

This subverts the entire proof with a partial function, be careful
Haskell is a proof minefield tbh, but a good way to be somewhat more sure is with {-# OPTIONS_GHC -Wincomplete-patterns #-}

This was my first proof :D