for k being Nat
for f being non constant standard special_circular_sequence st 1 <= k & k + 1 <= len f holds
Int (left_cell (f,k)) misses L~ f