let m, n be Nat; :: thesis: ( m ^2 = n ^2 implies m = n )
assume A1: m ^2 = n ^2 ; :: thesis: m = n

per cases ( m = n or m = - n ) by A1, SQUARE_1:40;

suppose m = n ; :: thesis: m = n

hence m = n ; :: thesis: verum

end;

suppose A2: m = - n ; :: thesis: m = n

then m = - 0 ;
hence m = n by A2; :: thesis: verum

end;

end;