n+k patterns

Could those in charge of the formal semantics of Haskell (yes,
that's you folks in Glasgow!) tell me what the meaning of n+k patterns
are?

In the report it says that

        case e0 of { x+k -> e; _ -> e' }

translates to

        if e0 >= k then { let { x' = e0-k } in e[x'/x] else e'

Which >= and - does this refer to?

What if they have been locally rebound?  E.g.

        let x - y = x ++ f y
                where f 0 = []
                      f (n+1) = f n
        in  [] - 0

Does the translated - still refer to the method in PreludeCore or
to the - in scope?

        -- Lennart

PS. I'd like to start the "Ban n+k patterns"-movement, any followers?