Every proof and lemma

1184 modules and 4,025 theorems, generated from the open core at 1.4.1. Each theorem is marked by what it covers: for all inputs (2,620), holds by unfolding a definition (236), or a worked example (1,169). What these mean.

Folder	Modules	Theorems
Non-negative rationals	140	315
Graph algorithms	8	25
Signed rationals	136	366
Finite sums	37	134
Data types	1	0
Finite types, distributions and Markov chains	122	582
Algorithm guarantees	85	295
Rationals	4	26
The Applied Higher-Order Functions catalogue	322	1,083
Analysis	6	17
Natural numbers	29	114
Sets	16	77
Binary numerals	2	0
Lemmas behind operations-research checks	104	264
Foundations	8	30
Vectors	44	141
Finite sets	5	27
Logic	15	67
Matrices	100	462