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

suppose a is odd ; :: thesis: a + (Parity a) is even

hence a + (Parity a) is even ; :: thesis: verum

end;

suppose a is even ; :: thesis: a + (Parity a) is even

hence a + (Parity a) is even ; :: thesis: verum

end;

end;