mathlib3

6d0adfa7 - feat(geometry/euclidean/angle/sphere): law of sines, converse of inscribed angles (#17992)

feat(geometry/euclidean/angle/sphere): law of sines, converse of inscribed angles (#17992) Add some (oriented angle) versions of the law of sines / sine rule, and of the converse of angles in the same segment / opposite angles of a cyclic quadrilateral. As with previous lemmas in this area, more versions would be appropriate to add in future, including unoriented angle versions and versions of the law of sines that don't involve the circumradius and so can be applied even in the degenerate case of collinear points, but this seems a reasonable starting point.