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

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