Changes

Summary

1. reoriented congruence rules in non-explosive direction
2. more fine-grained type class hierarchy for div and mod
3. restructured matter on polynomials and normalized fractions
4. streamlined computation rules for primality of numerals: no need to go via explicit conversion to nat
5. tuned fact references
6. clarified library contents
7. standardized notation
8. redundant
9. renewed and spread FIXME tags on watering bin interpretation, which got partially lost in 9f089287687b
10. added lemmas demanded by FIXMEs
11. dropped comment after conversation with author: predicate compiler works independently from any code generator setup
12. unconditional Code_Test_PolyML and Code_Test_Scala: compiler is always present;
13. tuned signature -- suppress pointless exports;
14. tuned;
15. more standard pretty printing; tuned messages;
16. tuned;
17. tuned whitespace; tuned comments;