Empty geometric sectors of a literal clockwise realization

The inverse rotation successor is the next counterclockwise outgoing germ. The open sector between these germs contains no other incident germ, at every finite degree.

theorem Cslib.Complexity.Graph.PolygonalDrawing.Realizes.not_sbtw_inverse_rotate {G : Graph} {D : G.PolygonalDrawing} {r : G.RotationSystem} (hR : D.Realizes r) (d e : G.Dart) (hvertex : e.vertex = d.vertex) (hed : e ≠ d) (heprev : e ≠ (Equiv.symm r.rotate) d) : ¬sbtw (D.direction d) (D.direction e) (D.direction ((Equiv.symm r.rotate) d))

Literal clockwise realization makes the inverse-rotation sector empty.