Theorem Fin.castSucc_le_castSucc_iff

Modification history