let h be non constant standard special_circular_sequence; :: thesis: n_e_n h <> n_e_s h

set i1 = n_e_n h;

set i2 = n_e_s h;

A1: n_e_n h <= (n_e_n h) + 1 by NAT_1:11;

A2: 1 <= n_e_n h by Def16;

(n_e_n h) + 1 <= len h by Def16;

then n_e_n h <= len h by A1, XXREAL_0:2;

then n_e_n h in dom h by A2, FINSEQ_3:25;

then A3: h . (n_e_n h) = h /. (n_e_n h) by PARTFUN1:def 6;

A4: n_e_s h <= (n_e_s h) + 1 by NAT_1:11;

A5: h . (n_e_s h) = S-max (L~ h) by Def14;

A6: 1 <= n_e_s h by Def14;

(n_e_s h) + 1 <= len h by Def14;

then n_e_s h <= len h by A4, XXREAL_0:2;

then n_e_s h in dom h by A6, FINSEQ_3:25;

then A7: h . (n_e_s h) = h /. (n_e_s h) by PARTFUN1:def 6;

A8: h . (n_e_n h) = N-max (L~ h) by Def16;

thus n_e_n h <> n_e_s h :: thesis: verum

set i1 = n_e_n h;

set i2 = n_e_s h;

A1: n_e_n h <= (n_e_n h) + 1 by NAT_1:11;

A2: 1 <= n_e_n h by Def16;

(n_e_n h) + 1 <= len h by Def16;

then n_e_n h <= len h by A1, XXREAL_0:2;

then n_e_n h in dom h by A2, FINSEQ_3:25;

then A3: h . (n_e_n h) = h /. (n_e_n h) by PARTFUN1:def 6;

A4: n_e_s h <= (n_e_s h) + 1 by NAT_1:11;

A5: h . (n_e_s h) = S-max (L~ h) by Def14;

A6: 1 <= n_e_s h by Def14;

(n_e_s h) + 1 <= len h by Def14;

then n_e_s h <= len h by A4, XXREAL_0:2;

then n_e_s h in dom h by A6, FINSEQ_3:25;

then A7: h . (n_e_s h) = h /. (n_e_s h) by PARTFUN1:def 6;

A8: h . (n_e_n h) = N-max (L~ h) by Def16;

thus n_e_n h <> n_e_s h :: thesis: verum

proof

assume
n_e_n h = n_e_s h
; :: thesis: contradiction

then A9: N-bound (L~ h) = (h /. (n_e_s h)) `2 by A8, A3, EUCLID:52

.= S-bound (L~ h) by A5, A7, EUCLID:52 ;

A10: 1 <= len h by GOBOARD7:34, XXREAL_0:2;

then A11: (h /. 1) `2 >= S-bound (L~ h) by Th11;

consider ii being Nat such that

A12: ii in dom h and

A13: (h /. ii) `2 <> (h /. 1) `2 by GOBOARD7:31;

A14: ii <= len h by A12, FINSEQ_3:25;

A15: 1 <= ii by A12, FINSEQ_3:25;

then A16: (h /. ii) `2 <= N-bound (L~ h) by A14, Th11;

A17: (h /. ii) `2 >= S-bound (L~ h) by A15, A14, Th11;

(h /. 1) `2 <= N-bound (L~ h) by A10, Th11;

then (h /. 1) `2 = N-bound (L~ h) by A9, A11, XXREAL_0:1;

hence contradiction by A9, A13, A16, A17, XXREAL_0:1; :: thesis: verum

end;then A9: N-bound (L~ h) = (h /. (n_e_s h)) `2 by A8, A3, EUCLID:52

.= S-bound (L~ h) by A5, A7, EUCLID:52 ;

A10: 1 <= len h by GOBOARD7:34, XXREAL_0:2;

then A11: (h /. 1) `2 >= S-bound (L~ h) by Th11;

consider ii being Nat such that

A12: ii in dom h and

A13: (h /. ii) `2 <> (h /. 1) `2 by GOBOARD7:31;

A14: ii <= len h by A12, FINSEQ_3:25;

A15: 1 <= ii by A12, FINSEQ_3:25;

then A16: (h /. ii) `2 <= N-bound (L~ h) by A14, Th11;

A17: (h /. ii) `2 >= S-bound (L~ h) by A15, A14, Th11;

(h /. 1) `2 <= N-bound (L~ h) by A10, Th11;

then (h /. 1) `2 = N-bound (L~ h) by A9, A11, XXREAL_0:1;

hence contradiction by A9, A13, A16, A17, XXREAL_0:1; :: thesis: verum