feat(order/cover): `f a` covers `f b` iff `a` covers `b`  (#11392)
feat(order/cover): `f a` covers `f b` iff `a` covers `b`  (#11392)

... for order isomorphisms, and also weaker statements.

Co-authored-by: Vladimir Ivanov <da39a3ee5e6b4b0d3255bfef95601890afd80709@astOwOlfo>





leanprover-community/mathlib,leanprover-community/mathlib