( nat : Type )

---

( 0 : nat )
( suc : nat -> nat )

---

( nat_eq : nat -> nat -> Prop )

( nat_eq_0 : ?? (nat_eq 0 0) )
( nat_eq_suc : ?? {i,j : nat} (nat_eq i j) -> (nat_eq (suc i) (suc j)) )

( nat_not_eq_0_suc : ?? {i : nat} (Not (nat_eq 0 (suc i))) )
( nat_not_eq_suc_0 : ?? {i : nat} (Not (nat_eq (suc i) 0)) )
( nat_not_eq_suc_suc : ?? {i,j : nat} (Not (nat_eq i j)) -> (Not (nat_eq (suc i) (suc j))) )

---

( nat_plus : nat -> nat -> nat ) 

( nat_plus_comm : || {i,j : nat} ((nat_plus i j) = (nat_plus j i)) )
( nat_plus_assoc : || {i,j,k : nat} ((nat_plus i (nat_plus j k)) = (nat_plus (nat_plus i j) k)) )

( nat_plus_0 : !! {i : nat} ((nat_plus i 0) = i) )
( nat_plus_suc : !! {i,j : nat} ((nat_plus i (suc j)) = (suc (nat_plus i j))) )

---

( nat_minus : nat -> nat -> nat )

( nat_minus_0 : !! {i : nat} ((nat_minus i 0) = i) )
( nat_minus_suc : !! {i,j : nat} ((nat_minus (suc i) (suc j)) = (nat_minus i j)) )

---

( nat_mult : nat -> nat -> nat )

( nat_mult_comm : || {i,j : nat} ((nat_mult i j) = (nat_mult j i)) )
( nat_mult_assoc : || {i,j,k : nat} ((nat_mult i (nat_mult j k)) = (nat_mult (nat_mult i j) k)) )

( nat_mult_0 : !! {i : nat} ((nat_mult 0 i) = 0) )
( nat_mult_1 : !! {i : nat} ((nat_mult (suc 0) i) = i) )
( nat_mult_suc : !! {i,j : nat} ((nat_mult i (suc j)) = (nat_plus i (nat_mult i j))) )

---

( nat_le : nat -> nat -> Prop )

( nat_le_0 : ?? {i : nat} (nat_le 0 i) )
( nat_le_suc : ?? {i,j : nat} (nat_le i j) -> (nat_le (suc i) (suc j)) )

--- ( nat_le_refl : ?? {i : nat} (nat_le i i) )
--- ( nat_le_suc' : ?? {i,j : nat} (nat_le i j) -> (nat_le i (suc j)) )

( nat_not_le_imp_le : {n,k : nat} (Not (nat_le n k)) -> (nat_le k n) )
( nat_le_le_imp_eq : {n,k : nat} (nat_le n k) -> (nat_le k n) -> (k = n) )
( nat_not_le_not_le_false : {n,k : nat} (Not (nat_le n k)) -> (Not (nat_le k n)) -> False )

---

( nat_lt : nat -> nat -> Prop )

( nat_lt_ax : ?? {i,j : nat} (Not (nat_eq i j)) -> (nat_le i j) -> (nat_lt i j) )

---

( nat_lt_imp_not_le : ?? {i,j : nat} (nat_lt j i) -> (Not (nat_le i j)) )

---

( nat_fact : nat -> nat )

( nat_fact_0 : !! ((nat_fact 0) = (suc 0)) )
( nat_fact_suc : !! {n : nat} ((nat_fact (suc n)) = (nat_mult (suc n) (nat_fact n))) )

---

( nat_ind : {P : nat -> Prop} 
            (P 0) -> 
            ({i : nat} (P i) -> (P (suc i))) ->
            {n : nat} (P n) )

( done )