Mordor OpenTheory Repo

packages   •   recent   •   upload

Package natural-1.16

Information

For more details see the package document.

Includes

• axiom-infinity-1.2 — Axiom of Infinity
• natural-pre-1.4 — natural-pre
• natural-add-1.12 — Definitions and theorems about natural number addition
• natural-cases-1.4 — natural-cases
• natural-def-1.5 — natural-def
• natural-distance-1.6 — Natural number distance function
• natural-div-mod-1.6 — Definitions and theorems about natural number division
• natural-even-odd-1.5 — Definitions and theorems about natural number even and odd
• natural-exp-1.6 — Definitions and theorems about natural number exponentiation
• natural-factorial-1.6 — Definitions and theorems about natural number factorial
• natural-min-max-1.8 — Natural number min and max functions
• natural-mult-1.11 — Definitions and theorems about natural number multiplication
• natural-numeral-1.5 — Definitions and theorems about natural number numerals
• natural-order-1.9 — Definitions and theorems about natural number orderings
• natural-recursion-1.3 — natural-recursion
• natural-sub-1.6 — Definitions and theorems about natural number subtraction

Included By

• base-1.28 — The standard theory library