mathlib

cbf81dff - archive(imo1988_q6): a formalization of Q6 on IMO1988 (#1455)

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