The second line would be read "0 <= x" implies "x == y". Implies is a boolean operator with lower precedence than && or ||; it is used in postconditions ("ensures") to make claims that are conditioned on other things. This allows more flexible preconditions and postconditions, without requiring the coder to enter the main body of a function and write traditional conditional expressions before stating the pre/postconditions.
Consider this snippet of dafny code from http://rise4fun.com/Dafny/tutorial/guide:
The second line would be read "0 <= x" implies "x == y". Implies is a boolean operator with lower precedence than && or ||; it is used in postconditions ("ensures") to make claims that are conditioned on other things. This allows more flexible preconditions and postconditions, without requiring the coder to enter the main body of a function and write traditional conditional expressions before stating the pre/postconditions.