(SqF n) |^ 2 divides n by Skup;
then TSqF n divides n by Cosik;
then n = (TSqF n) * (n div (TSqF n)) by NAT_D:3;
hence n div (TSqF n) is non zero Nat ; :: thesis: verum