Theorem Fin.succAbove_of_le_castSucc

Modification history