Summary
- minimum of maintainability for proof
- tuned proofs
- dropped various legacy fact bindings and tuned proofs
- separated potentially conflicting type class instance into separate theory
- accommodated gcd instances for polynomials
- more sophisticated GCD syntax
- dropped various legacy fact bindings
- prefer abbreviations for compound operators INFIMUM and SUPREMUM