theorem EuclidGeom.Triangle.IsCongr.unique_of_eq_eq {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr₁ : EuclidGeom.Triangle P} {tr₂ : EuclidGeom.Triangle P} (h : EuclidGeom.Triangle.IsCongr tr₁ tr₂) (p₁ : tr₁.point₁ = tr₂.point₁) (p₂ : tr₁.point₂ = tr₂.point₂) [hne : EuclidGeom.PtNe tr₁.point₁ tr₁.point₂] : tr₁.point₃ = tr₂.point₃

theorem EuclidGeom.acongr_of_AAS_variant {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd₁ : EuclidGeom.TriangleND P) (tr_nd₂ : EuclidGeom.TriangleND P) (a₁ : tr_nd₁.angle₁.dvalue = -tr_nd₂.angle₁.dvalue) (a₂ : tr_nd₁.angle₂.value = -tr_nd₂.angle₂.value) (e₃ : tr_nd₁.edge₁.length = tr_nd₂.edge₁.length) : EuclidGeom.HasACongr.acongr tr_nd₁ tr_nd₂

theorem EuclidGeom.acongr_of_AAS' {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd₁ : EuclidGeom.TriangleND P) (tr_nd₂ : EuclidGeom.TriangleND P) (a₁ : tr_nd₁.angle₁.value = -tr_nd₂.angle₁.value) (a₂ : tr_nd₁.angle₂.value = -tr_nd₂.angle₂.value) (e₃ : tr_nd₁.edge₁.length = tr_nd₂.edge₁.length) : EuclidGeom.HasACongr.acongr tr_nd₁ tr_nd₂

theorem EuclidGeom.congr_of_perm_congr {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.TriangleND.IsCongr (EuclidGeom.TriangleND.perm_vertices tr_nd₁) (EuclidGeom.TriangleND.perm_vertices tr_nd₂)) : EuclidGeom.HasCongr.congr tr_nd₁ tr_nd₂

theorem EuclidGeom.acongr_of_perm_acongr {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr_nd₁ : EuclidGeom.TriangleND P} {tr_nd₂ : EuclidGeom.TriangleND P} (h : EuclidGeom.TriangleND.IsACongr (EuclidGeom.TriangleND.perm_vertices tr_nd₁) (EuclidGeom.TriangleND.perm_vertices tr_nd₂)) : EuclidGeom.HasACongr.acongr tr_nd₁ tr_nd₂