prove perpendicular from inner product zero

EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular.lean

@@ -101,4 +101,31 @@ theorem dist_pt_line_shortest (A B : P) {l : Line P} (h : B LiesOn l) : dist A B
 
 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]
+  unfold Dir.rotate
+  erw [Proj.map_vecND_toProj]
+  simp
+  erw [VecND.toProj_eq_toProj_iff]
+  obtain ⟨ ⟨ xv, yv ⟩, hv ⟩ := v
+  obtain ⟨ ⟨ xw, yw ⟩, hw ⟩ := w
+  rw [Vec.real_inner_apply] at h
+  simp at h ⊢
+  have : xw ≠ 0 ∨ yw ≠ 0 := by
+    contrapose! hw
+    obtain ⟨rfl, rfl⟩ := hw
+    rfl
+  rcases this with (h | h)
+  · use yv / xw
+    field_simp
+    linarith
+  · use -xv / yw
+    field_simp
+    linarith
+
+end Perpendicular_inner_product
+
 end EuclidGeom