Theorem Imo2024Q3.Condition.k_lt_of_big

Modification history