let k, n be natural Number ; :: thesis: ( n mod k = k - 1 implies (n + 1) mod k = 0 )
per cases ( k <> 0 or k = 0 ) ;
suppose k <> 0 ; :: thesis: ( n mod k = k - 1 implies (n + 1) mod k = 0 )
then k >= 1 by NAT_1:14;
then reconsider K = k - 1 as Element of NAT by INT_1:3, XREAL_1:48;
A1: K + 1 = k - 0 ;
assume n mod k = k - 1 ; :: thesis: (n + 1) mod k = 0
then (n + 1) mod k = k mod k by A1, Th22;
hence (n + 1) mod k = 0 by Th25; :: thesis: verum
end;
suppose k = 0 ; :: thesis: ( n mod k = k - 1 implies (n + 1) mod k = 0 )
hence ( n mod k = k - 1 implies (n + 1) mod k = 0 ) ; :: thesis: verum
end;
end;