Erdős 97 convex-octagon formalization: Pentagon #
theorem
Erdos97Octagon.no_unit_pentagon_centre
{o a b c d e : Plane}
{R : ℝ}
(hR : 0 < R)
(oa : dist o a = R)
(ob : dist o b = R)
(oc : dist o c = R)
(od : dist o d = R)
(oe : dist o e = R)
(ab : dist a b = R)
(bc : dist b c = R)
(cd : dist c d = R)
(de : dist d e = R)
(ea : dist e a = R)
:
Five equal chords cannot form an odd cycle on a circle with the same radius.