theorem LimId: :: MOEBIUS2:22

lim invNAT = 0