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 that
A1: k <= n and
A2: k >= 1 ; :: thesis: (k - 1) mod n = k - 1
A3: k - 1 >= 1 - 1 by A2, XREAL_1:9;
A4: n - 1 < n by XREAL_1:44;
k - 1 <= n - 1 by A1, XREAL_1:9;
then k - 1 < n by A4, XXREAL_0:2;
hence (k - 1) mod n = k - 1 by A3, NAT_D:63; :: thesis: verum