let n, i, j be Nat; :: thesis: ( i in Seg n & j in Seg n & i + j <> n + 1 implies ((i + j) - 1) mod n in Seg n )
assume B0: ( i in Seg n & j in Seg n ) ; :: thesis: ( not i + j <> n + 1 or ((i + j) - 1) mod n in Seg n )
assume i + j <> n + 1 ; :: thesis: ((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 A4: i + j < n + 1 ; :: thesis: ((i + j) - 1) mod n in Seg n

( 1 <= i & 1 <= j ) by B0, FINSEQ_1:1;
then 1 + 1 <= i + j by XREAL_1:7;
then A5: (1 + 1) - 1 <= (i + j) - 1 by XREAL_1:9;
A6: (i + j) - 1 < (n + 1) - 1 by A4, XREAL_1:9;
A7: ((i + j) - 1) mod n = (i + j) - 1 by A5, A6, NAT_D:63;
((i + j) - 1) mod n in NAT by A5, A7, INT_1:3;
hence ((i + j) - 1) mod n in Seg n by A5, A7, A6; :: thesis: verum

end;

suppose A10: i + j > n + 1 ; :: thesis: ((i + j) - 1) mod n in Seg n

(i + j) - n > (n + 1) - n by A10, XREAL_1:9;
then A11: ((i + j) - n) - 1 > 1 - 1 by XREAL_1:9;
A12: ((i + j) - n) - 1 >= 0 + 1 by A11, INT_1:7;
( i <= n & j <= n ) by B0, FINSEQ_1:1;
then i + j <= n + n by XREAL_1:7;
then (i + j) - n <= (n + n) - n by XREAL_1:9;
then A13: ((i + j) - n) - 1 <= n - 1 by XREAL_1:9;
n - 1 < n by XREAL_1:44;
then A14: ((i + j) - n) - 1 < n by A13, XXREAL_0:2;
A15: (((i + j) - n) - 1) mod n = ((i + j) - n) - 1 by A11, A14, NAT_D:63;
A16: (((i + j) - n) - 1) mod n in NAT by A11, A15, 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 A15, INT_1:50 ;
hence ((i + j) - 1) mod n in Seg n by A14, A15, A12, A16; :: thesis: verum

end;

end;