[Agda] Stranga konduto !

[Roman]

Agda's patter matching is top-down left-to-right, so she first tries
to unify `diag x (suc y)` with `diag zero zero = zero` (since its the
first equation for `diag`), but `x` is not in whnf, so `diag x (suc
y)` is stuck and doesn't reduce further. You can simply make the third
equation first:

diag : ℕ → ℕ → ℕ
diag x (suc y) = suc (diag (suc x) y)
diag zero zero = zero
diag (suc x) zero = suc (x + diag x zero)