Two_Lines_Meet_at_Unique_Point
Provedlinesproofwiki
Let two straight line segments be constructed on a straight line segment from its endpoints so that they meet at a point. Then there cannot be two other straight line segments equal to the former two respectively, constructed on the same straight line segment and on the same side of it, meeting at a different point.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Two_Lines_Meet_at_Unique_Point (a1 b1 c1 a2 b2 c2 : ℝ) (h : a1 * b2 ≠ a2 * b1) : ∃! p : ℝ × ℝ, a1 * p.1 + b1 * p.2 = c1 ∧ a2 * p.1 + b2 * p.2 = c2 := by sorry
Source