Library Coq.Reals.Rtrigo_facts
Bounds of expressions with trigonometric functions
Express trigonometric functions with each other
Express sin and cos with each other
Express tan with sin and cos
Note: tan_sin_Rabs wouldn't make a lot of sense, because one would need Rabs on both sides
Express sin and cos with tan
Additional shift lemmas for sin, cos, tan