let f be V22() standard special_circular_sequence; :: thesis: LeftComp f <> RightComp f
set g = Rotate (f,(N-min (L~ f)));
A1: L~ f = L~ (Rotate (f,(N-min (L~ f)))) by REVROT_1:33;
N-min (L~ f) in rng f by SPRECT_2:39;
then A2: (Rotate (f,(N-min (L~ f)))) /. 1 = N-min (L~ (Rotate (f,(N-min (L~ f))))) by A1, FINSEQ_6:92;
A3: RightComp (Rotate (f,(N-min (L~ f)))) = RightComp f by REVROT_1:37;
LeftComp (Rotate (f,(N-min (L~ f)))) = LeftComp f by REVROT_1:36;
hence LeftComp f <> RightComp f by A2, A3, Lm2; :: thesis: verum