let a be Integer; :: thesis: parity a = parity (- a)

per cases ( a is even or a is odd ) ;

suppose A1: a is even ; :: thesis: parity a = parity (- a)

0 is even ;
then 0 - a is even by A1;
hence parity a = parity (- a) by A1; :: thesis: verum

end;

suppose A1: a is odd ; :: thesis: parity a = parity (- a)

then - a is odd ;
hence parity a = parity (- a) by A1; :: thesis: verum

end;

end;