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:3, XREAL_1:48;
n mod k < (k - 1) + 1 by A1, 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 Th2; :: 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 Th1; :: thesis: verum

end;

end;