[Agda] Nat arithmetic properties

[Roman]

Sergei, yes, {-# OPTIONS --no-eta-equality #-} — for a whole file, and
for records it looks like this:

    record R : Set where
      no-eta-equality
      constructor C
      field
         ...