prove perpendicular from inner product zero

EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular.lean

@@ -105,4 +105,45 @@ theorem eq_dist_eq_perp_foot {A B : P} {l : DirLine P} (h : A LiesOn l) (heq : d
 
 end Perpendicular_constructions
 
+section Perpendicular_inner_product
+
+theorem perp_of_inner_product_eq_zero (v w : VecND) (h : inner v.1 w.1 = (0 : ℝ)) : v ⟂ w := by
+  unfold perpendicular Proj.perp
+  rw [Proj.vadd_coe_left]
+  erw [Proj.map_vecND_toProj]
+  simp only [Dir.map_apply, ne_eq, LinearEquiv.restrictScalars_apply, VecND.toDir_toProj]
+  erw [VecND.toProj_eq_toProj_iff]
+  obtain ⟨ ⟨ xv, yv ⟩, hv ⟩ := v
+  obtain ⟨ ⟨ xw, yw ⟩, hw ⟩ := w
+  rw [Vec.real_inner_apply] at h
+  simp only [Vec.rotate_mk, AngValue.cos_coe, Real.cos_pi_div_two, zero_mul, AngValue.sin_coe, Real.sin_pi_div_two, one_mul, zero_sub, zero_add, Vec.smul_mk, mul_neg, Vec.mk.injEq] at h ⊢
+  have : xw ≠ 0 ∨ yw ≠ 0 := by
+    contrapose! hw
+    obtain ⟨rfl, rfl⟩ := hw
+    rfl
+  rcases this
+  · use yv / xw
+    field_simp
+    linarith
+  · use -xv / yw
+    field_simp
+    linarith
+
+theorem inner_product_eq_zero_of_perp (v w : VecND) (h : v ⟂ w) : inner v.1 w.1 = (0 : ℝ) := by
+  unfold perpendicular Proj.perp at h
+  rw [Proj.vadd_coe_left] at h
+  erw [Proj.map_vecND_toProj] at h
+  simp only [Dir.map_apply, ne_eq, LinearEquiv.restrictScalars_apply, VecND.toDir_toProj] at h 
+  erw [VecND.toProj_eq_toProj_iff] at h
+  obtain ⟨ ⟨ xv, yv ⟩, hv ⟩ := v
+  obtain ⟨ ⟨ xw, yw ⟩, hw ⟩ := w
+  rw [Vec.real_inner_apply]
+  simp only [Vec.rotate_mk, AngValue.cos_coe, Real.cos_pi_div_two, zero_mul, AngValue.sin_coe, Real.sin_pi_div_two, one_mul, zero_sub, zero_add, Vec.smul_mk, mul_neg, Vec.mk.injEq] at h ⊢
+  obtain ⟨a, ⟨ h₁, h₂ ⟩⟩ := h
+  rw [h₁, h₂]
+  linarith
+
+
+end Perpendicular_inner_product
+
 end EuclidGeom