let k, n be natural Number ; :: thesis: ( n mod k < k - 1 implies (n + 1) mod k = (n mod k) + 1 )
assume n mod k < k - 1 ; :: thesis: (n + 1) mod k = (n mod k) + 1
then A1: (n mod k) + 1 < k by XREAL_1:20;
(n + 1) mod k = ((n mod k) + 1) mod k by Th22;
hence (n + 1) mod k = (n mod k) + 1 by A1, Th24; :: thesis: verum