@@ -153,6 +153,7 @@ This has been normalised to ``0 = 0`` so now we have to prove that ``0`` equals
153is easy to prove by reflexivity from the pruviloj library:
153is easy to prove by reflexivity from the pruviloj library:
155.. code-block:: idris
155.. code-block:: idris
156 -Main.plusredZ_Z> reflexivity
157 -Main.plusredZ_Z> reflexivity
157 plusredZ_Z: No more goals.
158 plusredZ_Z: No more goals.