Theorem toIocMod_sub_natCast_mul

Modification history