:sat \(x : Bit) (y : Bit) -> x < y
:prove \(x : Bit) (y : Bit) -> x <= y || y <= x