module Subtraction where

open import Preliminaries
open import IntegerAlgebra

subtraction-alg : ℤ → IntAlg ℤ
subtraction-alg x .IntAlg.S = inv-iso ℤ.S
subtraction-alg x .IntAlg.Z = x

_-_ : ℤ → ℤ → ℤ
_-_ x = ℤ-rec (subtraction-alg x)

sub-S : {x y : ℤ} → x - ℤ.S .fun y ≡ ℤ.S .inv (x - y)
sub-S {x} {y} = ℤ-rec-S (subtraction-alg x) y

sub-Z : {x : ℤ} → x - ℤ.Z ≡ x
sub-Z {x} = ℤ-rec-Z (subtraction-alg x)

S-sub-S : {x y : ℤ} → ℤ.S .fun x - ℤ.S .fun y ≡ x - y
S-sub-S {x} {y} = ℤ-rec-uniq (subtraction-alg x) (λ y → sub-S)
  (sub-S • ap (ℤ.S .inv) sub-Z • ℤ.S .inv-fun x) (λ y → sub-S) sub-Z y

sub-self : {x : ℤ} → x - x ≡ ℤ.Z
sub-self {x} = ℤ-ind (mk-DIntAlg (eq-congr (symm S-sub-S) refl) sub-Z) x