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 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;