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 A1: ( 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 A2: i + j < n + 1 ; :: thesis: ((i + j) - 1) mod n in Seg n

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

end;

suppose A6: i + j > n + 1 ; :: thesis: ((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; :: thesis: verum

end;

end;