mathlib3

a5347cb9 - feat(*): add various order-related lemmas (#16918)

feat(*): add various order-related lemmas (#16918) These all came up while preparing to introduce the definition of ergodic maps but it seems better to PR them separately. Co-authored-by: Johan Commelin <johan@commelin.net>