let n be natural number ; :: thesis: ( n <> 1 implies n |-count 1 = 0 )
assume A1: 1 <> n ; :: thesis: n |-count 1 = 0

A2: now

assume A3: n |^ (0 + 1) divides 1 ; :: thesis: contradiction
then n |^ 1 <= 1 by NAT_D:7;
then n <= 1 by NEWTON:10;
then n = 0 by A1, NAT_1:26;
then 0 divides 1 by A3, NEWTON:10;
hence contradiction by INT_2:3; :: thesis: verum

end;

n |^ 0 divides 1 by NEWTON:9;
hence n |-count 1 = 0 by A1, A2, Def7; :: thesis: verum