module DepthComonads.Nat.Properties where

open import DepthComonads.Prelude
open import DepthComonads.Nat
open import DepthComonads.Algebra
open import DepthComonads.Bool

private variable n m : ℕ

+-assoc : Associative _+_
+-assoc zero    y z = refl
+-assoc (suc x) y z = cong suc (+-assoc x y z)

+0 : ∀ x → x +  ≡ x
+0 zero = refl
+0 (suc x) = cong suc (+0 x)

pred : ℕ → ℕ
pred zero = zero
pred (suc n) = n

suc-inj : suc n ≡ suc m → n ≡ m
suc-inj = cong pred

is-zero : ℕ → Bool
is-zero zero    = true
is-zero (suc n) = false

zero≢suc : zero ≢ suc n
zero≢suc = true≢false ∘ cong is-zero