theorem EuclidGeom.Triangle.cosine_rule' {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) [hab : EuclidGeom.PtNe B A] [hac : EuclidGeom.PtNe C A] : 2 * (‖VEC_nd A B‖ * ‖VEC_nd A C‖ * EuclidGeom.AngValue.cos (EuclidGeom.VecND.angle (VEC_nd A B) (VEC_nd A C))) = { source := A, target := B }.length ^ 2 + { source := A, target := C }.length ^ 2 - { source := B, target := C }.length ^ 2

theorem EuclidGeom.Triangle.cosine_rule {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : 2 * (tr_nd.edge₃.length * tr_nd.edge₂.length * EuclidGeom.AngValue.cos tr_nd.angle₁.value) = tr_nd.edge₃.length ^ 2 + tr_nd.edge₂.length ^ 2 - tr_nd.edge₁.length ^ 2

theorem EuclidGeom.Triangle.cosine_rule'' {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : tr_nd.edge₁.length = (tr_nd.edge₃.length ^ 2 + tr_nd.edge₂.length ^ 2 - 2 * (tr_nd.edge₃.length * tr_nd.edge₂.length * EuclidGeom.AngValue.cos tr_nd.angle₁.value)) ^ (1 / 2)

theorem EuclidGeom.Triangle.sine_rule₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : tr_nd.edge₂.length * EuclidGeom.AngValue.sin tr_nd.angle₃.value = tr_nd.edge₃.length * EuclidGeom.AngValue.sin tr_nd.angle₂.value

theorem EuclidGeom.Triangle.sine_rule₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : tr_nd.edge₁.length * EuclidGeom.AngValue.sin tr_nd.angle₃.value = tr_nd.edge₃.length * EuclidGeom.AngValue.sin tr_nd.angle₁.value

theorem EuclidGeom.Triangle.sine_rule₃ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) : tr_nd.edge₂.length * EuclidGeom.AngValue.sin tr_nd.angle₁.value = tr_nd.edge₁.length * EuclidGeom.AngValue.sin tr_nd.angle₂.value

theorem EuclidGeom.Pythagoras_of_ne_ne_perp {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} (hab : B ≠ A) (hac : C ≠ A) (h : { val := { source := A, target := B }, property := hab }.toProj.perp = { val := { source := A, target := C }, property := hac }.toProj) : { source := A, target := B }.length ^ 2 + { source := A, target := C }.length ^ 2 = { source := B, target := C }.length ^ 2

theorem EuclidGeom.Pythagoras_of_perp_foot {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) {l : EuclidGeom.Line P} (h : EuclidGeom.lies_on B l) : { source := A, target := EuclidGeom.perp_foot A l }.length ^ 2 + { source := B, target := EuclidGeom.perp_foot A l }.length ^ 2 = { source := A, target := B }.length ^ 2

theorem EuclidGeom.Pythagoras_of_right_triangle_non_trivial {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) {hnd : ¬EuclidGeom.Collinear A B C} (right_triangle : ∠ B A C (_ : B ≠ A) (_ : C ≠ A) = ∠[Real.pi / 2]) : { source := A, target := B }.length ^ 2 + { source := A, target := C }.length ^ 2 = { source := B, target := C }.length ^ 2

Given ▵ A B C with ∠ B A C = π / 2, A B ^ 2 + A C ^ 2 = B C ^ 2, namely (SEG A B).length ^ 2 + (SEG A C).length ^ 2 = (SEG B C).length ^ 2.

theorem EuclidGeom.Pythagoras_of_tr_nd {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) (h : tr_nd.angle₁.value = ∠[Real.pi / 2] ∨ tr_nd.angle₁.value = ∠[-Real.pi / 2]) : tr_nd.edge₂.length ^ 2 + tr_nd.edge₃.length ^ 2 = tr_nd.edge₁.length ^ 2