Construction_of_Equilateral_Triangle
Provedconstructionseuclidean-geometryproofwiki
Given a line segment AB, one can construct an equilateral triangle ABC (Euclid Book I Proposition 1).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Construction_of_Equilateral_Triangle (A B : ℝ × ℝ) (h : A ≠ B) : ∃ C : ℝ × ℝ, dist A C = dist A B ∧ dist B C = dist A B := by sorry
Source