Documentation Verification Report

PSub

📁 Source: Mathlib/Data/Nat/PSub.lean

Statistics

Metric	Count
Definitions `ppred`, `psub`, `psub'`	3
Theorems `ppred_eq_none`, `ppred_eq_pred`, `ppred_eq_some`, `ppred_succ`, `ppred_zero`, `pred_eq_ppred`, `psub'_eq_psub`, `psub_add`, `psub_eq_none`, `psub_eq_some`, `psub_eq_sub`, `psub_succ`, `psub_zero`, `sub_eq_psub`	14
Total	17

Nat

Definitions

Name	Category	Theorems
`ppred` 📖	CompOp	9 math math: `Partrec.ppred`, `pred_eq_ppred`, `psub_succ`, `ppred_succ`, `ppred_eq_pred`, `ppred_eq_some`, `Num.ppred_to_nat`, `ppred_eq_none`, `ppred_zero`
`psub` 📖	CompOp	8 math math: `psub_zero`, `psub_succ`, `psub_eq_some`, `psub_add`, `psub'_eq_psub`, `psub_eq_sub`, `psub_eq_none`, `sub_eq_psub`
`psub'` 📖	CompOp	1 math math: `psub'_eq_psub`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ppred_eq_none` 📖	mathematical	—	`ppred`	—	—
`ppred_eq_pred` 📖	mathematical	—	`ppred`	—	`ppred_eq_some`
`ppred_eq_some` 📖	mathematical	—	`ppred`	—	—
`ppred_succ` 📖	mathematical	—	`ppred`	—	—
`ppred_zero` 📖	mathematical	—	`ppred`	—	—
`pred_eq_ppred` 📖	mathematical	—	`ppred`	—	—
`psub'_eq_psub` 📖	mathematical	—	`psub'` `psub`	—	`psub'.eq_1` `psub_eq_sub` `psub_eq_none` `not_le`
`psub_add` 📖	mathematical	—	`psub`	—	`add_zero`
`psub_eq_none` 📖	mathematical	—	`psub`	—	`lt_of_not_ge` `psub_eq_some` `add_comm`
`psub_eq_some` 📖	mathematical	—	`psub`	—	`add_zero` `add_comm` `add_left_comm`
`psub_eq_sub` 📖	mathematical	—	`psub`	—	`psub_eq_some`
`psub_succ` 📖	mathematical	—	`psub` `ppred`	—	—
`psub_zero` 📖	mathematical	—	`psub`	—	—
`sub_eq_psub` 📖	mathematical	—	`psub`	—	`pred_eq_ppred` `psub.eq_2`

---

← Back to Index