Theorem Order.succ_lt_succ_iff_of_not_isMax

Modification history