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

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;

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;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