Theorem toIocMod_sub_ofNat_mul'

Modification history