let n, i, j be Nat; :: thesis: ( 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 ; :: thesis: ((j - i) mod n) + 1 in Seg n
( i <= n & 1 <= j ) by A1, A2, FINSEQ_1:3;
then A3: 1 - n <= j - i by XREAL_1:15;
( 1 <= i & j <= n ) by A1, A2, FINSEQ_1:3;
then A4: j - i <= n - 1 by XREAL_1:15;
- n <= (- n) + 1 by XREAL_1:31;
then A5: - n <= j - i by A3, XXREAL_0:2;
n - 1 < n by XREAL_1:46;
then A6: j - i < n by A4, XXREAL_0:2;
(j - i) mod n <= n - 1

proof

per cases ( 0 <= j - i or 0 > j - i ) ;

suppose 0 <= j - i ; :: thesis: (j - i) mod n <= n - 1

hence (j - i) mod n <= n - 1 by A4, A6, INT_3:10; :: thesis: verum

end;

suppose A7: 0 > j - i ; :: thesis: (j - i) mod n <= n - 1

then j - i <= - 1 by INT_1:21;
then n + (j - i) <= n + (- 1) by XREAL_1:8;
hence (j - i) mod n <= n - 1 by A5, A7, INT_3:10; :: thesis: verum

end;

end;

end;

then A8: ((j - i) mod n) + 1 <= (n - 1) + 1 by XREAL_1:8;
n in NAT by ORDINAL1:def 13;
then n > 0 by A1, FINTOPO5:2;
then (j - i) mod n >= 0 by INT_3:9;
then ( ((j - i) mod n) + 1 >= 0 + 1 & ((j - i) mod n) + 1 in NAT ) by INT_1:16, XREAL_1:8;
hence ((j - i) mod n) + 1 in Seg n by A8; :: thesis: verum