∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y z : V},
  y ≠ 0 →
    (InnerProductGeometry.angle x z = InnerProductGeometry.angle x y + InnerProductGeometry.angle y z ↔
      InnerProductGeometry.angle x z = Real.pi ∨ y ∈ Submodule.span NNReal {x, z})