mathlib3

refactor(strict_mono): make definition + move to order_functions

#998

Merged