module My.SetTheory.Nat.Cancellation where

-- §──────────────────────────────────────────────────────────────────
-- Required modules
-- §──────────────────────────────────────────────────────────────────

import Algebra as A
import Data.Nat as DN
import Data.Nat.Properties as DNP
import Function as F
import Relation.Binary.PropositionalEquality as RBPE

open DN using (_+_ ; _*_)
open F using (_$_)
open RBPE using (_≡_)

-- §──────────────────────────────────────────────────────────────────
-- Right cancellation for addition.  Left cancellation for addition is
-- DNP.cancel-+-left .
-- §──────────────────────────────────────────────────────────────────

cancel-+-right : (x y : DN.ℕ) → {n : DN.ℕ} → x + n ≡ y + n → x ≡ y
cancel-+-right x y {n} x+n≡y+n = x≡y
  where
    n+x≡n+y : n + x ≡ n + y
    n+x≡n+y =
      begin
        n + x ≡⟨ CSR.+-comm n x ⟩
        x + n ≡⟨ x+n≡y+n ⟩
        y + n ≡⟨ CSR.+-comm y n ⟩
        n + y ∎
      where
        module CSR = A.CommutativeSemiring DNP.commutativeSemiring
        open RBPE.≡-Reasoning
    x≡y : x ≡ y
    x≡y = DNP.cancel-+-left n n+x≡n+y

-- §──────────────────────────────────────────────────────────────────
-- Left cancellation for multiplication of non-zero nats.  Right
-- cancellation for such multiplication is DNP.cancel-*-right .
-- §──────────────────────────────────────────────────────────────────

cancel-*-left : (n : DN.ℕ) → {x y : DN.ℕ} → DN.suc n * x ≡ DN.suc n * y → x ≡ y
cancel-*-left n {x} {y} sn*x≡sn*y = x≡y
  where
    x*sn≡y*sn : x * DN.suc n ≡ y * DN.suc n
    x*sn≡y*sn =
      begin
        x * DN.suc n ≡⟨ CSR.*-comm x $ DN.suc n ⟩
        DN.suc n * x ≡⟨ sn*x≡sn*y ⟩
        DN.suc n * y ≡⟨ CSR.*-comm (DN.suc n) y ⟩
        y * DN.suc n ∎
      where
        module CSR = A.CommutativeSemiring DNP.commutativeSemiring
        open RBPE.≡-Reasoning
    x≡y : x ≡ y
    x≡y = DNP.cancel-*-right x y x*sn≡y*sn