let n be Nat; :: thesis: for z being non zero Nat holds
not for k being Nat holds not n = (z * k) + 0 & ... & not n = (z * k) + (z - 1)
let z be non zero Nat; :: thesis: not for k being Nat holds not n = (z * k) + 0 & ... & not n = (z * k) + (z - 1)

per cases ( z - 1 <= n or n < z - 1 ) ;

suppose A1: z - 1 <= n ; :: thesis: not for k being Nat holds not n = (z * k) + 0 & ... & not n = (z * k) + (z - 1)

not not n, 0 are_congruent_mod z & ... & not n,z - 1 are_congruent_mod z by NAT_6:13;
then consider i being Nat such that
0 <= i and
A2: i <= z - 1 and
A3: n,i are_congruent_mod z ;
consider k being Integer such that
A4: z * k = n - i by A3;
n - (z - 1) >= n - n by A1, XREAL_1:10;
then z * k >= 0 by A2, A4, XREAL_1:10;
then not k is negative ;
then reconsider k = k as Nat by TARSKI:1;
take k ; :: thesis: not not n = (z * k) + 0 & ... & not n = (z * k) + (z - 1)
thus not not n = (z * k) + 0 & ... & not n = (z * k) + (z - 1) :: thesis: verum

proof

take i ; :: thesis: ( 0 <= i & i <= z - 1 & n = (z * k) + i )
thus ( 0 <= i & i <= z - 1 & n = (z * k) + i ) by A2, A4; :: thesis: verum

end;

end;

suppose A5: n < z - 1 ; :: thesis: not for k being Nat holds not n = (z * k) + 0 & ... & not n = (z * k) + (z - 1)

take k = 0 ; :: thesis: not not n = (z * k) + 0 & ... & not n = (z * k) + (z - 1)
thus not not n = (z * k) + 0 & ... & not n = (z * k) + (z - 1) :: thesis: verum

proof

take n ; :: thesis: ( 0 <= n & n <= z - 1 & n = (z * k) + n )
thus ( 0 <= n & n <= z - 1 & n = (z * k) + n ) by A5; :: thesis: verum

end;

end;

end;