# Documentation

Mathlib.Data.Nat.PSub

# Partial predecessor and partial subtraction on the natural numbers #

The usual definition of natural number subtraction (Nat.sub) returns 0 as a "garbage value" for a - b when a < b. Similarly, Nat.pred 0 is defined to be 0. The functions in this file wrap the result in an Option type instead:

## Main definitions #

• Nat.ppred: a partial predecessor operation
• Nat.psub: a partial subtraction operation
def Nat.ppred :

Partial predecessor operation. Returns ppred n = some m if n = m + 1, otherwise none.

Instances For
@[simp]
theorem Nat.ppred_zero :
= none
@[simp]
theorem Nat.ppred_succ {n : } :
= some n
def Nat.psub (m : ) :

Partial subtraction operation. Returns psub m n = some k if m = n + k, otherwise none.

Equations
Instances For
@[simp]
theorem Nat.psub_zero {m : } :
@[simp]
theorem Nat.psub_succ {m : } {n : } :
Nat.psub m () =
theorem Nat.sub_eq_psub (m : ) (n : ) :
m - n = Option.getD (Nat.psub m n) 0
@[simp]
theorem Nat.ppred_eq_some {m : } {n : } :
= some m = n
@[simp]
theorem Nat.ppred_eq_none {n : } :
= none n = 0
theorem Nat.psub_eq_some {m : } {n : } {k : } :
Nat.psub m n = some k k + n = m
theorem Nat.psub_eq_none {m : } {n : } :
Nat.psub m n = none m < n
theorem Nat.ppred_eq_pred {n : } (h : 0 < n) :
= some ()
theorem Nat.psub_eq_sub {m : } {n : } (h : n m) :
Nat.psub m n = some (m - n)
theorem Nat.psub_add (m : ) (n : ) (k : ) :
Nat.psub m (n + k) = do let __do_lift ← Nat.psub m n Nat.psub __do_lift k
@[inline]
def Nat.psub' (m : ) (n : ) :

Same as psub, but with a more efficient implementation.

Instances For
theorem Nat.psub'_eq_psub (m : ) (n : ) :
= Nat.psub m n