NOTE: the latest version is 13.0.0

README About Versions Source Modules

Nat.N

modify

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

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

The NNat plus 1.

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

Nat

(N

(Nat1Plus nMinus1)

Is

(Difference a To (Nat1Plus nMinus1PlusA))

)

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

The NNat minus 1.

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

Modules