let n, i be Nat; :: thesis: ( i in Seg n implies (n + 1) - i in Seg n )

assume A1: i in Seg n ; :: thesis: (n + 1) - i in Seg n

i <= n by A1, FINSEQ_1:1;

then i + 1 <= n + 1 by XREAL_1:6;

then A2: (i + 1) - i <= (n + 1) - i by XREAL_1:9;

1 <= i by A1, FINSEQ_1:1;

then n + 1 <= i + n by XREAL_1:6;

then A3: (n + 1) - i <= (i + n) - i by XREAL_1:9;

(n + 1) - i in NAT by A2, INT_1:3;

hence (n + 1) - i in Seg n by A2, A3; :: thesis: verum

assume A1: i in Seg n ; :: thesis: (n + 1) - i in Seg n

i <= n by A1, FINSEQ_1:1;

then i + 1 <= n + 1 by XREAL_1:6;

then A2: (i + 1) - i <= (n + 1) - i by XREAL_1:9;

1 <= i by A1, FINSEQ_1:1;

then n + 1 <= i + n by XREAL_1:6;

then A3: (n + 1) - i <= (i + n) - i by XREAL_1:9;

(n + 1) - i in NAT by A2, INT_1:3;

hence (n + 1) - i in Seg n by A2, A3; :: thesis: verum