∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y z : V},
  InnerProductGeometry.angle x z = InnerProductGeometry.angle x y + InnerProductGeometry.angle y z →
    InnerProductGeometry.angle x z = 0 → InnerProductGeometry.angle x y = 0