Every proof and lemma

1196 modules and 4,030 theorems, generated from the open core at 1.5.5. Each theorem is marked by what it covers: for all inputs (2,622), holds by unfolding a definition (236), or a worked example (1,172). What these mean.

Folder	Modules	Theorems
Non-negative rationals	140	315
Graph algorithms	8	25
Signed rationals	147	366
Finite sums	37	134
Data types	1	0
Finite types, distributions and Markov chains	122	581
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	16	73
Matrices	100	462