[Agda] EqReasoning example

[Serge D. Mechveliani]

Please,
how to fix the below program using  EqReasoning ? 
I am trying  "begin ...",  and it does not type-check.

This short program is attached here as  Main.agda.zip.

The example is only for  n + 0 ~~ 0 + n   for n : Nat,
and the report is
------------------------------------------------------------
(n + 0 .Relation.Binary.Core.Dummy... 0 + n)

when checking that 0 are valid arguments to a function of type
(n + 0 .Relation.Binary.Core.Dummy.... 0 + n)
------------------------------------------------------------

Thanks,

------
Sergei
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Main.agda.zip
Type: application/zip
Size: 688 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20130304/c70a5b75/Main.agda.zip