let k, n be Nat; :: thesis: ( not k <> 0 or (n + 1) mod k = 0 or (n + 1) mod k = (n mod k) + 1 )
assume A1: k <> 0 ; :: thesis: ( (n + 1) mod k = 0 or (n + 1) mod k = (n mod k) + 1 )
then k >= 1 by NAT_1:14;
then reconsider K = k - 1 as Element of NAT by INT_1:16, XREAL_1:50;
k > 0 by A1;
then n mod k < (k - 1) + 1 by NAT_D:1;
then A2: n mod k <= K by NAT_1:13;

per cases ( n mod k < k - 1 or n mod k = k - 1 ) by A2, XXREAL_0:1;

suppose n mod k < k - 1 ; :: thesis: ( (n + 1) mod k = 0 or (n + 1) mod k = (n mod k) + 1 )

hence ( (n + 1) mod k = 0 or (n + 1) mod k = (n mod k) + 1 ) by A1, Th3; :: thesis: verum

end;

suppose n mod k = k - 1 ; :: thesis: ( (n + 1) mod k = 0 or (n + 1) mod k = (n mod k) + 1 )

hence ( (n + 1) mod k = 0 or (n + 1) mod k = (n mod k) + 1 ) by Th2; :: thesis: verum

end;

end;