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

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

structure EuclidGeom.Square (P : Type u_1) [EuclidGeom.EuclideanPlane P] extends EuclidGeom.Rhombus : Type u_1