let n be Integer; :: thesis: n * (n + 1) is even

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

suppose n is even ; :: thesis: n * (n + 1) is even

hence n * (n + 1) is even ; :: thesis: verum

end;

suppose n is odd ; :: thesis: n * (n + 1) is even

hence n * (n + 1) is even ; :: thesis: verum

end;

end;