# Nat

Nat package contains inductive data type definition representing Peano arithmetic.

```data nat = zero | suc (a: nat) ```

## zero

zero construction represent lowest nat number.

`> let a: nat = zero in a`
```EVAL: zero
```

## suc

suc constructor defines next nat number.

`> let a: nat = suc zero in a`
```EVAL: suc zero
```

# Generics

## pred: nat -> nat

Returns a nat predecessor.

`> pred (suc zero)`
```EVAL: zero
```

## add (m: nat) : nat -> nat

Returns an addendum.

# Instances

```equalNat : nat -> nat -> bool nat_instance : eq = (nat, equalNat) ```

# Theorems

```add_zero : (n : nat) -> Path nat (add zero n) n add_suc (a:nat) : (n : nat) -> Path nat (add (suc a) n) (suc (add a n)) add_comm (a : nat) : (n : nat) -> Path nat (add a n) (add n a) assocAdd (a b:nat) : (c:nat) -> Path nat (add a (add b c)) (add (add a b) c) sucInj (n m : nat) (p : Path nat (suc n) (suc m)) : Path nat n m add_comm3 (a b c : nat) : Path nat (add a (add b c)) (add c (add b a)) caseNat (A : U) (a0 aS : A) : nat -> A caseDNat (P:nat -> U) (a0 :P zero) (aS : (n:nat) -> P (suc n)) natDec : (n m:nat) -> dec (Path nat n m) natSet : isSet nat```