Use positive (nonzero) natural numbers

Some `PParams` ought to be positive natural numbers, as "enforced" by `paramsWellFormed`. E.g., `refScriptCostStride`.

In some cases, such as `refScriptCostStride`, this fact is _needed_ in some other parts of the code:

```agda
scriptsCost : (pp : PParams) → ℕ → Coin
scriptsCost pp scSz with (PParams.refScriptCostStride pp)
... | 0 = 0 -- This case should never occur; refScriptCostStride should always be > 0.
... | suc m =
scriptsCostAux 0ℚ
minFeeRefScriptCoinsPerByte scSz
(<′-wellFounded scSz)

```

I think it would make sense to define a type of positive naturals.