Construction_of_Equal_Straight_Lines_from_Unequal
Disprovedlinesproofwiki
Given two unequal straight line segments, it is possible to cut off from the greater a straight line segment equal to the lesser.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Construction_of_Equal_Straight_Lines_from_Unequal (a b : ℝ) (hab : a < b) : ∃ c : ℝ, 0 ≤ c ∧ c = a := by sorry
Source