| FTA | The Fundamental Theorem of Arithmetic - unique prime factorizability |
| IteratedBinops | Iterated Binary Operations |
| SimpleMulFacts | Some handy lemmas about integer multiplication. |
| num thy 1 | Elementary divisibility theory over the integers. Gcd function and relation introduced. Chinese remainder theorem proven. |
| union | Non canonical functions (isl, outl, outr) for union type. |
| int 2 | |
| LogicSupplement | Some handy basic lemmas about propositions and about types. |
| quot 1 | Support lemmas for quotient type. |
| rel 1 | Common properties of binary relations. |
| bool 1 | |
| int 1 | |
| well fnd | |
| core | Some basic concepts defined type-theoretically. |