let t be Integer; :: thesis: for k being positive Nat holds
( t mod k = k - 1 iff (t + 1) mod k = 0 )
let k be positive Nat; :: thesis: ( t mod k = k - 1 iff (t + 1) mod k = 0 )
thus ( t mod k = k - 1 implies (t + 1) mod k = 0 ) :: thesis: ( (t + 1) mod k = 0 implies t mod k = k - 1 )

proof

assume A1: t mod k = k - 1 ; :: thesis: (t + 1) mod k = 0
0 = (0 + (1 * k)) mod k
.= (1 + (t mod k)) mod k by A1
.= (1 + t) mod k by Th88 ;
hence (t + 1) mod k = 0 ; :: thesis: verum

end;

assume A1: (t + 1) mod k = 0 ; :: thesis: t mod k = k - 1
(k - 1) + 1 > (k - 1) + 0 by XREAL_1:6;
then k - 1 = ((k - 1) + ((t + 1) mod k)) mod k by A1, NAT_D:24
.= ((k - 1) + (t + 1)) mod k by Th88
.= (t + (1 * k)) mod k
.= t mod k by NAT_D:61 ;
hence t mod k = k - 1 ; :: thesis: verum