Commit 2019-10-16 18:45 cbf81dff
View on Github →archive(imo1988_q6): a formalization of Q6 on IMO1988 (#1455)
- archive(imo1988_q6): a formalization of Q6 on IMO1988
- WIP
- Clean up, document, and use omega
- Remove some non-terminal simps
- Non-terminal simp followed by ring is fine
- Include copyright statement
- Add comment justifying example
- Process review comments
- Oops, forgot a line
- Improve comments in the proof