module MiniLibrary.Natplus where

open import MiniLibrary.Base
open import MiniLibrary.Nat

data ℕ+ : Set where
 suc :   -> ℕ+

_<ℕ+b_ : ℕ+  -> ℕ+  -> Bool
suc n  <ℕ+b suc m = n <ℕb m

_<ℕ+_ : ℕ+  -> ℕ+  -> Set
n <ℕ+ m = True (n <ℕ+b m)

_≤ℕ+b_ : ℕ+  -> ℕ+  -> Bool
suc n  ≤ℕ+b suc m = n ≤ℕb m

_≤ℕ+_ : ℕ+  -> ℕ+  -> Set
n ≤ℕ+ m = True (n ≤ℕ+b m)


_==ℕ+b_ : ℕ+  -> ℕ+  -> Bool
suc n  ==ℕ+b suc m = n ==ℕb m

_==ℕ+_ : ℕ+  -> ℕ+  -> Set
n ==ℕ+ m = True (n ==ℕ+b m)

decideℕ+ : (n m : ℕ+)  n <ℕ+   m  n ==ℕ+  m  m <ℕ+  n
decideℕ+ (suc n) (suc m) = decideℕ n m

decideℕ+≤  : (n m : ℕ+)  n ≤ℕ+   m  m ≤ℕ+  n
decideℕ+≤  (suc n) (suc m) = decideℕ≤  n m


_+ℕ+_ : ℕ+  ℕ+  ℕ+
suc n +ℕ+ suc m = suc (suc  (n + m))

_*ℕ+_ : ℕ+  ℕ+  ℕ+
suc n *ℕ+ suc m = suc (n * m + n + m)



==impliesℕ+≤   : (n m : ℕ+)  (n ==ℕ+   m)  n ≤ℕ+  m
==impliesℕ+≤  (suc n)  (suc m)   p = ==impliesℕ≤  n  m   p  


ℕ+2ℕ : ℕ+  
ℕ+2ℕ (suc n) = suc n

{- ℕ2ℕ+ n returns max {1 , n} as an element of ℕ+ -}
ℕ2ℕ+ :   ℕ+
ℕ2ℕ+ zero     = suc zero
ℕ2ℕ+ (suc n)  = suc n


1ℕ+ : ℕ+
1ℕ+ = suc 0

2ℕ+ : ℕ+
2ℕ+ = suc 1

3ℕ+ : ℕ+
3ℕ+ = suc 2

4ℕ+ : ℕ+
4ℕ+ = suc 3