mathlib documentation

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

@[simp]
def nat.ppred  :

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

Equations
@[simp]
def nat.psub  :
option

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

Equations
theorem nat.sub_eq_psub (m n : ) :
m - n = (m.psub n).get_or_else 0

@[simp]
theorem nat.ppred_eq_some {m n : } :
n.ppred = some m m.succ = n

@[simp]
theorem nat.ppred_eq_none {n : } :
n.ppred = none n = 0

theorem nat.psub_eq_some {m n k : } :
m.psub n = some k k + n = m

theorem nat.psub_eq_none (m n : ) :
m.psub n = none m < n

theorem nat.ppred_eq_pred {n : } :
0 < nn.ppred = some n.pred

theorem nat.psub_eq_sub {m n : } :
n mm.psub n = some (m - n)

theorem nat.psub_add (m n k : ) :
m.psub (n + k) = m.psub n >>= λ (x : ), x.psub k