theorem Th9: :: NUMBER02:9

(- 1) mod 3 = 2