Erdős 97 convex-octagon formalization: Cycle Strip #
theorem
Erdos97Octagon.no_unit_cycle_square_strip
{o x1 x2 x3 x4 x5 x6 : Plane}
{R : ℝ}
(hR : 0 < R)
(e01 : dist o x1 = R)
(e02 : dist o x2 = R)
(e06 : dist o x6 = R)
(e12 : dist x1 x2 = R)
(e13 : dist x1 x3 = R)
(e23 : dist x2 x3 = R)
(e24 : dist x2 x4 = R)
(e34 : dist x3 x4 = R)
(e35 : dist x3 x5 = R)
(e45 : dist x4 x5 = R)
(e46 : dist x4 x6 = R)
(e56 : dist x5 x6 = R)
:
The twelve listed equal-length edges cannot form this planar cycle-square strip.