Reciprocal trigonometric functions

Stream: mathlib4

[Snir Broshi]

There are 3 basic trigonometric functions (sin/cos/tan), and 3 operations one can perform on them to get more functions- reciprocal, inverse, hyperbolic. This produces 3 * 2 * 2 * 2 = 24 functions.
Mathlib has 13 of these- the 12 non-reciprocal functions, plus docs#Complex.cot.
(artanh was recently added :)

Do you think we should add the missing 11, remove cot, or do nothing?
(it's actually adding 16 because non-inverses have a complex and a real version)

While it's easy to just write 1 / ..., an advantage of adding the functions is that HasSum csc ... looks better than HasSum (1 / sin) ... and in other theorems / trig identities, and makes the results easier to Loogle (standardizes spelling between 1 / sin and fun x ↦ 1 / sin x).

OTOH randomly adding 16 functions sounds weird, even if we include some easy trig identities about them.
(maybe proving their Taylor series expansion is enough of a non-trivial theorem to motivate adding them?)

Are these reciprocals used in papers / fancy theorems, or are they a math history relic that is not worth defining?