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;