Pattern match(es) are non-exhaustive in `gcd` function

For learning purposes, I am defining gcd' function in terms of repeated subtraction:

gcd' :: Integer -> Integer -> Integer
gcd' x y 
    | x == y = x
    | x < y = gcd' x (y - x)
    | y < x = gcd' (x - y) y

(Prelude's gcd function)

The problem is GHC complains about it:

Pattern match(es) are non-exhaustive. In an equation for ‘gcd'’:

Patterns of type ‘Integer’, ‘Integer’ not matched: _ _

I've seen a mathematical law concerning numbers which said:

For all numbers 𝑥 and 𝑦, it is true that either 𝑥 is less than 𝑦, or 𝑦 is less than 𝑥, or 𝑥 equals 𝑦.

In that sense, those three guards cover all possible scenarios. Why is GHC concerned about this definition ?

Pattern match(es) are non-exhaustive. In an equation for ‘gcd'’:

The problem is that Haskell is not that clever to know that for two items x and y, it always holds that x < y, x > y or x == y, and in fact it does not even hold. Indeed, for a NaN, it does not hold:

ghci> nan = 0/0
ghci> nan
NaN
ghci> nan == nan
False
ghci> nan > nan
False
ghci> nan < nan
False

It is better to work with a condition that is always true: otherwise, which is an alias for True:

gcd' :: Integer -> Integer -> Integer
gcd' x y 
    | x == y = x
    | x < y = gcd' x (y - x)
    | otherwise = gcd' (x - y) y

Note that a faster implementation of gcd' is:

gcd' :: Integral a => a -> a -> a
gcd' a b
  | b == 0 = a
  | otherwise = gcd' b (a `mod` b)