Nat.N

modify

Nat (N n (IsBoth a To nPlusA And b To nPlusB))

-> Nat

(Nat1Plus n)

(IsBoth a To (Nat1Plus nPlusA) And b To (Nat1Plus nPlusB))

)

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)

(IsBoth

(Nat1Plus nMinus1PlusA)

And

(Nat1Plus nMinus1PlusB)

)

-> Nat

(N nMinus1 (IsBoth a To nMinus1PlusA And b To nMinus1PlusB))

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 isDifference) -> 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 a To nPlusA)) -> Nat (In n nPlusA)

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

The minimum is n, the maximum >= n.