Theorem Ordinal.mod_opow_log_lt_self

Modification history