ℕ+ is the type of positive natural numbers. It is defined as a subtype, and the VM representation of ℕ+ is the same as ℕ because the proof is not stored.

Convert a natural number to a positive natural number. The positivity assumption is inferred by dec_trivial.

Write a successor as an element of ℕ+.

Convert a natural number to a pnat. n+1 is mapped to itself, and 0 becomes 1.

We now define a long list of structures on ℕ+ induced by similar structures on ℕ. Most of these behave in a completely obvious way, but there are a few things to be said about subtraction, division and powers.

Subtraction a - b is defined in the obvious way when a > b, and by a - b = 1 if a ≤ b.

We define m % k and m / k in the same way as for nat except that when m = n * k we take m % k = k and m / k = n - 1. This ensures that m % k is always positive and m = (m % k) + k * (m / k) in all cases. Later we define a function div_exact which gives the usual m / k in the case where k divides m.