Construction_of_Equal_Straight_Line
Provedconstructionseuclidean-geometryproofwiki
Given a point P and a line segment AB, one can construct a point Q such that PQ = AB (Euclid Book I Proposition 2).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Construction_of_Equal_Straight_Line (P : ℝ × ℝ) (A B : ℝ × ℝ) (hAB : A ≠ B) : ∃ Q : ℝ × ℝ, dist P Q = dist A B := by sorry
Source