Commit 2022-11-30 21:59 e48be15a

View on Github →

feat: port Data.Nat.PSub (#806) mathlib3 SHA: 62a5626868683c104774de8d85b9855234ac807c I'm not sure if the file should be called Psub.lean or PSub.lean - mathport chooses the former.

Estimated changes

added def Nat.ppred
added theorem Nat.ppred_eq_none
added theorem Nat.ppred_eq_pred
added theorem Nat.ppred_eq_some
added theorem Nat.ppred_succ
added theorem Nat.ppred_zero
added theorem Nat.pred_eq_ppred
added def Nat.psub'
added theorem Nat.psub'_eq_psub
added def Nat.psub
added theorem Nat.psub_add
added theorem Nat.psub_eq_none
added theorem Nat.psub_eq_some
added theorem Nat.psub_eq_sub
added theorem Nat.psub_succ
added theorem Nat.psub_zero
added theorem Nat.sub_eq_psub