feat(geometry/euclidean): angles and some basic lemmas (#2865)
Define angles (undirected, between 0 and π, in terms of inner
product), and prove some basic lemmas involving angles, for real inner
product spaces and Euclidean affine spaces.
From the 100-theorems list, this provides versions of
* 04 Pythagorean Theorem,
* 65 Isosceles Triangle Theorem and
* 94 The Law of Cosines, with various existing definitions implicitly providing
* 91 The Triangle Inequality.
