From Max_is_some and Max_is_ge, one can prove that ge is a total relation.
So the consequents hold even if "ge x y" does not (since "ge y x" then
holds by totality).