Theorem Fin.castSucc_lt_castSucc_iff

Modification history