theorem EuclidGeom.perp_of_angle_dvalue_eq_pi_div_two {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} [h1 : EuclidGeom.PtNe B A] [h2 : EuclidGeom.PtNe C A] (h : (ANG B A C).dvalue = ↑∠[Real.pi / 2]) : EuclidGeom.Perpendicular (LIN B A) (LIN C A)