-- File: nat2

-- defines eq, +, and max

Path "../lol"
Load "nat"

--------
-- eq --
--------

Def eq := iternat (\n:Nat. isZero n) (\eq_Pm:Nat->Bool. 
          primrecnat false (\Pn:Nat. \dummy:Bool. eq_Pm Pn))

Prove eq_O_O : eq O O = true

Prove eq_O_Sm : @m:Nat. eq O (S m) = false

Prove eq_Sm_O : @m:Nat. eq (S m) O = false

Prove eq_Sm_Sn : @m,n:Nat. eq (S m) (S n) = eq m n

Prove eq__Eq : @m,n:Nat. eq m n = true -> m=n

Prove eq_m_m : @m:Nat. eq m m = true

Prove eq_m_n : @m,n:Nat. Not (m=n) -> eq m n = false

Prove Not_eq__Not_Eq : @m,n:Nat. eq m n = false -> Not (m=n)


----------
-- plus --
----------

-- Name in lemmas: plus
Def (+) := \m:Nat.\n:Nat. iternat n S m : Nat->Nat->Nat
Infix 5 (+)

Prove O_plus : @n:Nat. O+n = n

Prove Sm_plus : @m,n:Nat. S m + n = S (m + n)
    
Prove plus_O : @n:Nat. n+O = n



Prove plus_Sm : @m,n:Nat. m + S n = S (m+n)


Prove plus_comm : @m,n:Nat. m+n = n+m


Prove plus_assoc : @m,n,p:Nat. (m+n)+p = m+(n+p)



InfixR 5 (+)


---------
-- max --
---------

Def max := \m,n:Nat. if (leq n m) m n

Prove Le_max1 : @m,n:Nat. m <= max m n 

Prove max_comm : @m,n:Nat. max m n = max n m

Prove Le_max2 : @m,n:Nat. n <= max m n 

Prove max_assoc : @m,n,p:Nat. max (max m n) p = max m (max n p)