let f be non constant standard special_circular_sequence; :: thesis: for k being Nat st 1 <= k & k + 1 <= len f holds

Int (right_cell (f,k)) <> {}

let k be Nat; :: thesis: ( 1 <= k & k + 1 <= len f implies Int (right_cell (f,k)) <> {} )

assume that

A1: 1 <= k and

A2: k + 1 <= len f ; :: thesis: Int (right_cell (f,k)) <> {}

A3: len f = len (Rev f) by FINSEQ_5:def 3;

k <= len f by A2, NAT_1:13;

then A4: ((len f) -' k) + k = len f by XREAL_1:235;

then A5: ((len f) -' k) + 1 <= len f by A1, XREAL_1:6;

A6: (len f) -' k >= 1 by A2, A4, XREAL_1:6;

then right_cell (f,k) = left_cell ((Rev f),((len f) -' k)) by A1, A4, Th9;

hence Int (right_cell (f,k)) <> {} by A3, A5, A6, Th14; :: thesis: verum

Int (right_cell (f,k)) <> {}

let k be Nat; :: thesis: ( 1 <= k & k + 1 <= len f implies Int (right_cell (f,k)) <> {} )

assume that

A1: 1 <= k and

A2: k + 1 <= len f ; :: thesis: Int (right_cell (f,k)) <> {}

A3: len f = len (Rev f) by FINSEQ_5:def 3;

k <= len f by A2, NAT_1:13;

then A4: ((len f) -' k) + k = len f by XREAL_1:235;

then A5: ((len f) -' k) + 1 <= len f by A1, XREAL_1:6;

A6: (len f) -' k >= 1 by A2, A4, XREAL_1:6;

then right_cell (f,k) = left_cell ((Rev f),((len f) -' k)) by A1, A4, Th9;

hence Int (right_cell (f,k)) <> {} by A3, A5, A6, Th14; :: thesis: verum