begin
Lm1:
for f being non constant standard clockwise_oriented special_circular_sequence st f /. 1 = N-min (L~ f) holds
LeftComp f <> RightComp f
Lm2:
for f being non constant standard special_circular_sequence st f /. 1 = N-min (L~ f) holds
LeftComp f <> RightComp f