theorem PT1: :: NEWTON03:10
for a being non zero square Integer
for b being Integer st a * b is square holds
b is square