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: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
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, NAT_D:63; :: thesis: verum
end;
suppose A7: 0 > j - i ; :: thesis: (j - i) mod n <= n - 1
then j - i <= - 1 by INT_1:8;
then n + (j - i) <= n + (- 1) by XREAL_1:6;
hence (j - i) mod n <= n - 1 by A5, A7, NAT_D:63; :: thesis: verum
end;
end;
end;
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; :: thesis: verum