let n be Nat; :: thesis: ( n <> 1 implies n |-count 1 = 0 )
assume A1: 1 <> n ; :: thesis: n |-count 1 = 0
A2: now :: thesis: not n |^ (0 + 1) divides 1
assume A3: n |^ (0 + 1) divides 1 ; :: thesis: contradiction
then n |^ 1 <= 1 by NAT_D:7;
then n <= 1 ;
then n = 0 by A1, NAT_1:25;
then 0 divides 1 by A3;
hence contradiction ; :: thesis: verum
end;
n |^ 0 divides 1 by NEWTON:4;
hence n |-count 1 = 0 by A2, Def7; :: thesis: verum