let n be Nat; :: thesis: ( n divides 8 implies n in {1,2,4,8} )
assume A1: n divides 8 ; :: thesis: n in {1,2,4,8}
then n <= 8 by INT_2:27;
then A2: not not n = 0 & ... & not n = 8 ;
n <> 0 by A1;
then A3: 8 mod n = 0 by A1, INT_1:62;
( ((3 * 2) + 2) mod 3 = 2 mod 3 & ((5 * 1) + 3) mod 5 = 3 mod 5 & ((6 * 1) + 2) mod 6 = 2 mod 6 & ((7 * 1) + 1) mod 7 = 1 mod 7 ) by NAT_D:21;
hence n in {1,2,4,8} by A1, A2, A3, ENUMSET1:def 2, NAT_D:24; :: thesis: verum