feat(Order/RelIso): add theorems about RelHom.comp and RelEmbedding.trans (#37623)

Co-authored-by: SnirBroshi <26556598+SnirBroshi@users.noreply.github.com>

Author: IvanRenison

Mathlib/Order/RelIso/Basic.lean

@@ -144,6 +144,15 @@ protected def id (r : α → α → Prop) : r →r r :=
 protected def comp (g : s →r t) (f : r →r s) : r →r t :=
   ⟨fun x => g (f x), fun h => g.2 (f.2 h)⟩
 
+theorem comp_assoc (h : r →r s) (g : s →r t) (f : t →r u) :
+  (f.comp g).comp h = f.comp (g.comp h) := rfl
+
+@[simp]
+theorem comp_id (f : r →r s) : f.comp (RelHom.id r) = f := rfl
+
+@[simp]
+theorem id_comp (f : r →r s) : (RelHom.id s).comp f = f := rfl
+
 /-- A relation homomorphism is also a relation homomorphism between dual relations. -/
 @[simps]
 protected def swap (f : r →r s) : swap r →r swap s :=
@@ -277,6 +286,15 @@ theorem trans_apply (f : r ↪r s) (g : s ↪r t) (a : α) : (f.trans g) a = g (
 theorem coe_trans (f : r ↪r s) (g : s ↪r t) : (f.trans g) = g ∘ f :=
   rfl
 
+theorem trans_assoc (f : r ↪r s) (g : s ↪r t) (h : t ↪r u) :
+  (f.trans g).trans h = f.trans (g.trans h) := rfl
+
+@[simp]
+theorem trans_refl (f : r ↪r s) : f.trans (.refl s) = f := rfl
+
+@[simp]
+theorem refl_trans (f : r ↪r s) : .trans (.refl r) f = f := rfl
+
 /-- A relation embedding is also a relation embedding between dual relations. -/
 protected def swap (f : r ↪r s) : swap r ↪r swap s :=
   ⟨f.toEmbedding, f.map_rel_iff⟩