feat: more lemmas on Euclidean relations

[chenson2018]

A few more lemmas on Euclidean relations. Some other changes to note:

• The addition of Relation.{cod,dom}, mirroring what is done in Mathlib with SetRel but for unbundled relations. I am mulling over making a dedicated definition for restrictions of an unbundled relation, but wanted to have a few theorems to test with first.
• I change the name RightEuclidean.refl_range to RightEuclidean.refl_cod for naming consistency
• Using Relator.LeftTotal for the definition of Serial. None of the modal logic proofs change at all, as these are identical.

[ctchou]

An overall comment is that this file is getting large and probably should be split.

[ctchou]

Perhaps we can defined something like:

def RelInv r a b := r b a

Then the cod versions of many of these theorems can be derived from their dom versions plus properties of RelInv.

[chenson2018]

If taking this approach, I would have used the existing flip or Function.swap. They cause some problems that I attribute to there being a mismatch between core and Mathlib API. (Though maybe there's something more technical I've missed.) In a recent poll this form had more support, so I've tried to standardize on this approach, though I agree it is a bit ugly looking.

[chenson2018]

An overall comment is that this file is getting large and probably should be split.

Agreed. The limit in Mathlib is 1500 lines. I'll think about where best to split this as we approach that size in future PRs.