Summary
- reoriented congruence rules in non-explosive direction
- more fine-grained type class hierarchy for div and mod
- restructured matter on polynomials and normalized fractions
- streamlined computation rules for primality of numerals: no need to go via explicit conversion to nat
- tuned fact references
- clarified library contents
- standardized notation
- redundant
- renewed and spread FIXME tags on watering bin interpretation, which got partially lost in 9f089287687b
- added lemmas demanded by FIXMEs
- dropped comment after conversation with author: predicate compiler works independently from any code generator setup