mathlib

367d71ef - chore(order/iterate): review, add docs (#9965)

chore(order/iterate): review, add docs (#9965) * reorder sections; * add section docs; * use inequalities between functions in a few statements; * add a few lemmas about `strict_mono` functions.