The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

1/ To know what is really behind the notation, send the command:

Set Printing All.

and ask for the goal to be re-printed (for instance in console mode, 
just type Show 1.).

2/ Yes, you can avoid the proof by cases on p p0, you can even avoid 
induction on x and y
and get rid of the useless assumptions x <> 0 and y <> 0...

There is a combined tactic of less than 80 characters for this proof; 
here are a few hints:

1/ from (x + y = 0) omega can deduce (y = -x),
2/ Zabs_opp is your friend,

Yves