Martin Escardo, started 5th May 2018

\begin{code}

{-# OPTIONS --safe --without-K #-}

module Naturals.Subtraction where

open import MLTT.Spartan hiding (_^_ ; _+_)

open import Naturals.Addition
open import Naturals.Order
open import Naturals.Properties
open import Notation.Order

subtraction : (m n : ℕ) → m ≤ n → Σ k ꞉ ℕ , k + m ＝ n
subtraction         n        l = n , refl
subtraction (succ m)         l = 𝟘-elim l
subtraction (succ m) (succ n) l = pr₁ IH , ap succ (pr₂ IH)
 where
  IH : Σ k ꞉ ℕ , k + m ＝ n
  IH = subtraction m n l

cosubtraction : (m n : ℕ) → (Σ k ꞉ ℕ , k + m ＝ n) → m ≤ n
cosubtraction zero     _ (k , refl) = ⋆
cosubtraction (succ m) _ (k , refl) = cosubtraction m (k + m) (k , refl)

subtraction' : (x y : ℕ) → x < y → Σ z ꞉ ℕ , (z + x ＝ y)
subtraction'                 l = 𝟘-induction l
subtraction'         (succ y) l = (succ y) , refl
subtraction' (succ x)         l = 𝟘-elim l
subtraction' (succ x) (succ y) l = pr₁ IH , ap succ (pr₂ IH)
 where
  IH : Σ z ꞉ ℕ , z + x ＝ y
  IH = subtraction' x y l

subtraction'' : (x y : ℕ) → x < y → Σ z ꞉ ℕ , (succ z + x ＝ y)
subtraction'' x                l = 𝟘-elim l
subtraction''         (succ y) l = y , refl
subtraction'' (succ x) (succ y) l = pr₁ IH , ap succ (pr₂ IH)
 where
  IH : Σ z ꞉ ℕ , (succ z + x ＝ y)
  IH = subtraction'' x y l

\end{code}