mathlib3

7d417154 - feat(archive/imo/imo2008_q3): golf (#13232)