mathlib3

728baa2f - feat(archive/imo/imo2006_q5): IMO 2006 Q5 (#15613)

feat(archive/imo/imo2006_q5): IMO 2006 Q5 (#15613) See module docstring for a thorough explanation of the proof. Co-authored-by: Thomas Browning <tb65536@uw.edu>