mathlib3

3e2df830 - docs(order/order_iso_nat): Added note on `exists_increasing_or_nonincreasing_subseq` (#12239)