theorem Th7: :: NUMERAL2:7

EvenNAT misses OddNAT