let k, n be non zero Nat; :: thesis: ( k mod n = 0 implies (k - 1) mod n = n - 1 )
assume k mod n = 0 ; :: thesis: (k - 1) mod n = n - 1
then n divides k by PEPIN:6;
then consider m being Nat such that
A3: k = n * m by NAT_D:def 3;
A4: (n - 1) + 1 > (n - 1) + 0 by XREAL_1:6;
reconsider m = m as non zero Nat by A3;
reconsider d = m - 1 as Nat ;
((d * n) + (n - 1)) mod n = (n - 1) mod n by NAT_D:21
.= n - 1 by A4 ;
hence (k - 1) mod n = n - 1 by A3; :: thesis: verum