mathlib3

df5eddeb - refactor(strict_mono): make definition + move to order_functions (#998)

refactor(strict_mono): make definition + move to order_functions (#998) * refactor(strict_mono): make definition + move to order_functions * Weaken assumptions from preorder to has_lt