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

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

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