BasicTheorems
📁 Source: MRiscX/Util/BasicTheorems.lean
Statistics
Nat
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
add_gt_zero 📖 | — | — | — | — | add_gt_zero_gt_zero |
add_gt_zero_gt_zero 📖 | — | — | — | — | — |
gt_and_neq_succ_gt_succ 📖 | — | — | — | — | — |
gt_zero_le_one 📖 | — | — | — | — | — |
le_sub_one_le 📖 | — | — | — | — | — |
lt_add_cancel_right 📖 | — | — | — | — | — |
lt_sub_left 📖 | — | — | — | — | lt_add_cancel_right |
mod_succ_eq 📖 | — | — | — | — | — |
size_sub_lt_size 📖 | — | — | — | — | — |
UInt64
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
add_cancel_left_iff 📖 | — | — | — | — | add_cancel_right_iff |
add_cancel_right_iff 📖 | — | — | — | — | — |
add_lt_add 📖 | — | — | — | — | lt_toNat_iff |
add_right_ne_of_lt 📖 | — | — | — | — | add_cancel_left_iff |
add_sub_assoc 📖 | — | — | — | — | — |
gt_zero_neq_zero 📖 | — | — | — | — | — |
le_toNat_iff 📖 | — | — | — | — | — |
lt_toNat_iff 📖 | — | — | — | — | — |
lt_zero 📖 | — | — | — | — | — |
(root)
Definitions
| Name | Category | Theorems |
|---|---|---|
instPreorderUInt64_mRiscX 📖 | CompOp | — |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
excluded_middle_implication 📖 | — | — | — | — | — |
instWellFoundedLTUInt64_mRiscX 📖 | — | — | — | — | — |
---