( a - b is even & a + b is even ) ;
then 2 * 2 divides (a - b) * (a + b) by NEWTON03:5;
then 2 * 2 divides 2 * (((a |^ 2) - (b |^ 2)) / 2) by NEWTON01:1;
hence ((a |^ 2) - (b |^ 2)) / 2 is even by INT_4:7; :: thesis: verum