let n be Nat; :: thesis: Reci-Sqf . n >= 0

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: Reci-Sqf . n >= 0

hence Reci-Sqf . n >= 0 by MySumDef; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: Reci-Sqf . n >= 0

then reconsider nn = n as non zero Nat ;
Reci-Sqf . n = 1 / (SquarefreePart nn) by MySumDef;
hence Reci-Sqf . n >= 0 ; :: thesis: verum

end;

end;