let k, m be Nat; :: thesis: ( m <> 0 & (k + 1) mod m <> 0 implies (k + 1) mod m = (k mod m) + 1 )
assume C1: ( m <> 0 & (k + 1) mod m <> 0 ) ; :: thesis: (k + 1) mod m = (k mod m) + 1
(k mod m) + 1 <= m by NAT_D:1, C1, NAT_1:13;
then P1: ((k mod m) + 1) - 1 <= m - 1 by XREAL_1:9;
P2: (k + 1) mod m = ((k mod m) + 1) mod m by NAT_D:22;
k mod m < m - 1

proof

assume not k mod m < m - 1 ; :: thesis: contradiction
then (k + 1) mod m = ((m - 1) + 1) mod m by XXREAL_0:1, P1, P2
.= 0 by INT_1:50 ;
hence contradiction by C1; :: thesis: verum

end;

then (k mod m) + 1 < (m - 1) + 1 by XREAL_1:8;
hence (k + 1) mod m = (k mod m) + 1 by NAT_D:24, P2; :: thesis: verum