per cases ( a is square or not a is square ) ;
suppose a is square ; :: thesis: not a * (a - 1) is square
hence not a * (a - 1) is square ; :: thesis: verum
end;
suppose not a is square ; :: thesis: not a * (a - 1) is square
then reconsider a = a as non square Element of NAT ;
per cases ( a - 1 is square or not a - 1 is square ) ;
suppose a - 1 is square ; :: thesis: not a * (a - 1) is square
hence not a * (a - 1) is square ; :: thesis: verum
end;
suppose not a - 1 is square ; :: thesis: not a * (a - 1) is square
then reconsider k = a - 1 as non square Element of NAT by ORDINAL1:def 12;
a - 1,(a - 1) + 1 are_coprime ;
then not a * k is square by LmN30;
hence not a * (a - 1) is square ; :: thesis: verum
end;
end;
end;
end;