let n, k be Nat; :: 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 NAT_D:22;
hence (n + 1) mod k = (n mod k) + 1 by A1, NAT_D:24; :: thesis: verum