Std.Natural

Zero tests and ordering go through the ONE constant-time primitive the runtime offers on naturals, `nat-less-than`. A `nat-eliminate` over a natural is executed as a loop over its whole magnitude (measured 2026-09-16: asking whether the length of a 1 MiB string is zero cost 68 ms per call, about 65 ns per unit; the same question through nat-less-than costs nothing measurable), so no comparison may recurse on the value it compares. The 0/1 flag nat-less-than returns is the only thing eliminated.

62def naturalNonzero =
63  (lambda unrestricted value : Nat . (nat-less-than zero value))