let n, i, j be Nat; ( i in Seg n & j in Seg n & i + j <> n + 1 implies ((i + j) - 1) mod n in Seg n )
assume A1:
( i in Seg n & j in Seg n )
; ( not i + j <> n + 1 or ((i + j) - 1) mod n in Seg n )
assume
i + j <> n + 1
; ((i + j) - 1) mod n in Seg n
per cases then
( i + j < n + 1 or i + j > n + 1 )
by XXREAL_0:1;
suppose A6:
i + j > n + 1
;
((i + j) - 1) mod n in Seg n
(i + j) - n > (n + 1) - n
by A6, XREAL_1:9;
then A7:
((i + j) - n) - 1
> 1
- 1
by XREAL_1:9;
A8:
((i + j) - n) - 1
>= 0 + 1
by A7, INT_1:7;
(
i <= n &
j <= n )
by A1, FINSEQ_1:1;
then
i + j <= n + n
by XREAL_1:7;
then
(i + j) - n <= (n + n) - n
by XREAL_1:9;
then A9:
((i + j) - n) - 1
<= n - 1
by XREAL_1:9;
n - 1
< n
by XREAL_1:44;
then A10:
((i + j) - n) - 1
< n
by A9, XXREAL_0:2;
A11:
(((i + j) - n) - 1) mod n = ((i + j) - n) - 1
by A7, A10, NAT_D:63;
A12:
(((i + j) - n) - 1) mod n in NAT
by A7, A11, INT_1:3;
((i + j) - 1) mod n =
((((i + j) - 1) - n) + n) mod n
.=
(((((i + j) - 1) - n) mod n) + (n mod n)) mod n
by NAT_D:66
.=
((((i + j) - 1) - n) + 0) mod n
by A11, INT_1:50
;
hence
((i + j) - 1) mod n in Seg n
by A10, A11, A8, A12;
verum end;