Commit 2024-12-18 01:10 fb40f755

View on Github →

feat(Archive/Imo): formalize IMO 1982q3 (#16190) Formalize problem 3 of 1982 IMO. Co-authored by: Violeta Hernández Palacios vi.hdz.p@gmail.com

Estimated changes

added theorem Imo1982Q3.ineq
added theorem Imo1982Q3.le_avg
added theorem imo1982_q3a
added theorem imo1982_q3b
added theorem geom_sum_lt