theorem EuclidGeom.Trapezoid.ext {P : Type u_1} : ∀ {inst : EuclidGeom.EuclideanPlane P} (x y : EuclidGeom.Trapezoid P), x.point₁ = y.point₁ → x.point₂ = y.point₂ → x.point₃ = y.point₃ → x.point₄ = y.point₄ → x = y

theorem EuclidGeom.Trapezoid.ext_iff {P : Type u_1} : ∀ {inst : EuclidGeom.EuclideanPlane P} (x y : EuclidGeom.Trapezoid P), x = y ↔ x.point₁ = y.point₁ ∧ x.point₂ = y.point₂ ∧ x.point₃ = y.point₃ ∧ x.point₄ = y.point₄

structure EuclidGeom.Trapezoid (P : Type u_1) [EuclidGeom.EuclideanPlane P] extends EuclidGeom.Quadrilateral_cvx : Type u_1