{-# OPTIONS --cubical --no-import-sorts --no-exact-split --safe #-}
module Cubical.Data.NatPlusOne.Properties where

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

1+Path : ℕ ≡ ℕ₊₁
1+Path = isoToPath (iso 1+_ -1+_ (λ _ → refl) (λ _ → refl))

ℕ₊₁→ℕ-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

*₊₁-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)))