+lemma sub_comp_l: ∀A.∀R,R1,R2:relation A.
+ R1 ⊆ R2 → R1 ∘ R ⊆ R2 ∘ R.
+#A #R #R1 #R2 #Hsub #a #b * #c * /4/
+qed.
+
+lemma sub_comp_r: ∀A.∀R,R1,R2:relation A.
+ R1 ⊆ R2 → R ∘ R1 ⊆ R ∘ R2.
+#A #R #R1 #R2 #Hsub #a #b * #c * /4/
+qed.
+
+lemma sub_assoc_l: ∀A.∀R1,R2,R3:relation A.
+ R1 ∘ (R2 ∘ R3) ⊆ (R1 ∘ R2) ∘ R3.
+#A #R1 #R2 #R3 #a #b * #c * #Hac * #d * /5/
+qed.
+
+lemma sub_assoc_r: ∀A.∀R1,R2,R3:relation A.
+ (R1 ∘ R2) ∘ R3 ⊆ R1 ∘ (R2 ∘ R3).
+#A #R1 #R2 #R3 #a #b * #c * * #d * /5 width=5/
+qed.
+
+(************* functions ************)