mathlib3

feat(*): small lemmas from the sensitivity formalization

#1352

Merged