Theorem Imo2024Q3.ne_zero_of_M_le_apply

Modification history