let n be Element of NAT ; :: thesis: for k being Nat st k <= n & k >= 1 holds
(k - 1) mod n = k - 1
let k be Nat; :: thesis: ( k <= n & k >= 1 implies (k - 1) mod n = k - 1 )
assume A1: ( k <= n & k >= 1 ) ; :: thesis: (k - 1) mod n = k - 1
then A2: k - 1 <= n - 1 by XREAL_1:11;
n - 1 < n by XREAL_1:46;
then A5: k - 1 < n by A2, XXREAL_0:2;
k - 1 >= 1 - 1 by A1, XREAL_1:11;
hence (k - 1) mod n = k - 1 by A5, INT_3:10; :: thesis: verum