assume a - b is square ; :: thesis: contradiction
then reconsider c = a - b as odd square Integer ;
c + b = a ;
hence contradiction ; :: thesis: verum