{-# OPTIONS --no-exact-split #-}
module Cubical.Data.NatPlusOne.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Univalence
open import Cubical.Data.Nat
open import Cubical.Data.NatPlusOne.Base

open import Cubical.Reflection.StrictEquiv

1+Path : ℕ ≡ ℕ₊₁
1+Path = ua e
  where
  unquoteDecl e = declStrictEquiv e 1+_ -1+_

ℕ₊₁→ℕ-inj : ∀ {m n} → ℕ₊₁→ℕ m ≡ ℕ₊₁→ℕ n → m ≡ n
ℕ₊₁→ℕ-inj p i = 1+ (injSuc p i)

infixl  _·₊₁_

_·₊₁_ : ℕ₊₁ → ℕ₊₁ → ℕ₊₁
(1+ m) ·₊₁ (1+ n) = 1+ (n + m · (suc n))

private
  ℕ₊₁→ℕ-·₊₁-comm : ∀ m n → ℕ₊₁→ℕ (m ·₊₁ n) ≡ (ℕ₊₁→ℕ m) · (ℕ₊₁→ℕ n)
  ℕ₊₁→ℕ-·₊₁-comm (1+ m) (1+ n) = refl

+₁-assoc : ∀ m n o → m +₁ (n +₁ o) ≡ (m +₁ n) +₁ o
+₁-assoc one n o = refl
+₁-assoc (2+ m) n o = cong suc₊₁ (+₁-assoc (1+ m) n o)

·₊₁-comm : ∀ m n → m ·₊₁ n ≡ n ·₊₁ m
·₊₁-comm (1+ m) (1+ n) = cong 1+_ (injSuc (·-comm (suc m) (suc n)))

·₊₁-assoc : ∀ m n o → m ·₊₁ (n ·₊₁ o) ≡ m ·₊₁ n ·₊₁ o
·₊₁-assoc (1+ m) (1+ n) (1+ o) = cong 1+_ (injSuc (·-assoc (suc m) (suc n) (suc o)))

·₊₁-identityˡ : ∀ n →  ·₊₁ n ≡ n
·₊₁-identityˡ (1+ n) = cong 1+_ (injSuc (·-identityˡ (suc n)))

·₊₁-identityʳ : ∀ n → n ·₊₁  ≡ n
·₊₁-identityʳ (1+ n) = cong 1+_ (injSuc (·-identityʳ (suc n)))