(- 1) - (((- 1) div 3) * 3) = 2 by Th8;
hence (- 1) mod 3 = 2 by INT_1:def 10; :: thesis: verum