Nat.N

modify

Nat (N n Is (Difference a To nPlusA))

-> Nat (N (Nat1Plus n) Is (Difference a To (Nat1Plus nPlusA)))

The Nat (N ...) plus 1.

Keep in mind that if you want add any number, rather go for Nat (In ...) or Nat (Min ...).

Nat

(Nat1Plus nMinus1)

(Difference a To (Nat1Plus nMinus1PlusA))

)

-> Nat (N nMinus1 Is (Difference a To nMinus1PlusA))

The Nat (N ...) minus 1.

Keep in mind that if you want subtract any number, rather go for Nat (In ...) or Nat (Min ...).

toMin : Nat (N n Is difference) -> Nat (Min n)

Convert an exact Nat n to a Nat (Min n).

nat4 |> Nat.N.toMin
--> is of type Nat (Min Nat4)

toIn : Nat (N n Is (Difference a To nPlusA)) -> Nat (In n nPlusA)

A Nat (In ...) from an exact Nat (N n ...).

The minimum is n, the maximum >= n.