[Merged by Bors] - feat(Order/RelIso): add lemmas about congruence with relIso#37640

IvanRenison wants to merge 5 commits intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

IvanRenison:RelIso.relIsoCongrIvanRenison/mathlib4:RelIso.relIsoCongrCopy head branch name to clipboard