Erdős 97 convex-octagon formalization: Residual Algebra09

theorem Erdos97Octagon.residualRepresentative09_not_realises {p : Vertex → Plane} (hp : Function.Injective p) : ¬Realises p residualRepresentative09

Residual class 9 has no injective planar realisation.