let k, n be Nat; :: thesis: ( k <> 0 & n mod k < k - 1 implies (n + 1) mod k = (n mod k) + 1 )
assume ( k <> 0 & n mod k < k - 1 ) ; :: thesis: (n + 1) mod k = (n mod k) + 1
then A1: (n mod k) + 1 < k by XREAL_1:22;
(n + 1) mod k = ((n mod k) + 1) mod k by NAT_D:22;
hence (n + 1) mod k = (n mod k) + 1 by A1, NAT_D:24; :: thesis: verum