let n, i, j be Nat; ( i in Seg n & j in Seg n implies ((j - i) mod n) + 1 in Seg n )
assume that
A1:
i in Seg n
and
A2:
j in Seg n
; ((j - i) mod n) + 1 in Seg n
( i <= n & 1 <= j )
by A1, A2, FINSEQ_1:1;
then A3:
1 - n <= j - i
by XREAL_1:13;
( 1 <= i & j <= n )
by A1, A2, FINSEQ_1:1;
then A4:
j - i <= n - 1
by XREAL_1:13;
- n <= (- n) + 1
by XREAL_1:29;
then A5:
- n <= j - i
by A3, XXREAL_0:2;
n - 1 < n
by XREAL_1:44;
then A6:
j - i < n
by A4, XXREAL_0:2;
(j - i) mod n <= n - 1
then A8:
((j - i) mod n) + 1 <= (n - 1) + 1
by XREAL_1:6;
n > 0
by A1, FINTOPO5:2;
then
(j - i) mod n >= 0
by NAT_D:62;
then
( ((j - i) mod n) + 1 >= 0 + 1 & ((j - i) mod n) + 1 in NAT )
by INT_1:3, XREAL_1:6;
hence
((j - i) mod n) + 1 in Seg n
by A8; verum