let f be V22() standard special_circular_sequence; :: thesis: ( f /. 1 = N-min (L~ f) implies LeftComp f <> RightComp f )
assume A1: f /. 1 = N-min (L~ f) ; :: thesis: LeftComp f <> RightComp f
per cases ( f is clockwise_oriented or Rev f is clockwise_oriented ) by REVROT_1:38;
suppose f is clockwise_oriented ; :: thesis: LeftComp f <> RightComp f
hence LeftComp f <> RightComp f by A1, Lm1; :: thesis: verum
end;
suppose A2: Rev f is clockwise_oriented ; :: thesis: LeftComp f <> RightComp f
A3: LeftComp (Rev f) = RightComp f by GOBOARD9:23;
A4: RightComp (Rev f) = LeftComp f by GOBOARD9:24;
N-min (L~ (Rev f)) = N-min (L~ f) by SPPOL_2:22
.= (Rev f) /. (len f) by A1, FINSEQ_5:65
.= (Rev f) /. (len (Rev f)) by FINSEQ_5:def 3
.= (Rev f) /. 1 by FINSEQ_6:def 1 ;
hence LeftComp f <> RightComp f by A2, A3, A4, Lm1; :: thesis: verum
end;
end;