let k, m be Nat; :: thesis: ( m <> 0 & (k + 1) mod m = 0 implies m - 1 = k mod m )
assume C1: ( m <> 0 & (k + 1) mod m = 0 ) ; :: thesis: m - 1 = k mod m
then (k mod m) + 1 <= m by NAT_D:1, 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;
assume not k mod m = m - 1 ; :: thesis: contradiction
then k mod m < m - 1 by XXREAL_0:1, P1;
then (k mod m) + 1 < (m - 1) + 1 by XREAL_1:8;
hence contradiction by P2, NAT_D:24, C1; :: thesis: verum