let a, b be Integer; :: thesis: parity (a lcm b) = parity (a * b)

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

suppose A1: a * b is odd ; :: thesis: parity (a lcm b) = parity (a * b)

then ( a is odd & b is odd ) ;
then a lcm b is odd ;
hence parity (a lcm b) = parity (a * b) by A1; :: thesis: verum

end;

suppose A1: a * b is even ; :: thesis: parity (a lcm b) = parity (a * b)

then ( a is even or b is even ) ;
then a lcm b is even ;
hence parity (a lcm b) = parity (a * b) by A1; :: thesis: verum

end;

end;