mathlib

366fd9b1 - feat(analysis/special_functions): show (2 / π) * x ≤ sin x (#11724)

feat(analysis/special_functions): show (2 / π) * x ≤ sin x (#11724) I wasn't entirely sure where to put this - trigonometric/basic is too high on the import graph but here seems to work. This is a fairly weak inequality but it can sometimes turn out to be useful, and is important enough to be named!