Change variables order.

Add compose_eq and compose_id_{l,r}.

Lebesgue/Set_theory/Set_fun.v

@@ -106,19 +106,36 @@ Section Fun_Facts2.
 (** Facts about composition of functions. *)
 
 Context {U1 U2 U3 U4 : Type}.
-Variable f21 : U1 -> U2.
-Variable f32 : U2 -> U3.
 Variable f43 : U3 -> U4.
+Variable f32 : U2 -> U3.
+Variable f21 : U1 -> U2.
+
+Lemma compose_eq : forall (x1 : U1), compose f32 f21 x1 = f32 (f21 x1).
+Proof.
+easy.
+Qed.
 
 (* Useful? *)
 Lemma compose_assoc :
   compose3 f43 f32 f21 = compose (compose f43 f32) f21.
-Proof
+Proof.
+easy.
+Qed.
+
+(* Useful? *)
+Lemma compose_id_l : compose id f21 = f21.
+Proof.
+easy.
+Qed.
+
+(* Useful? *)
+Lemma compose_id_r : compose f32 id = f32.
+Proof.
 easy.
 Qed.
 
 Lemma image_compose_fun :
-  image (compose f32 f11) = fun A1 => image f32 (image f21 A1).
+  image (compose f32 f21) = fun A1 => image f32 (image f21 A1).
 Proof.
 apply fun_ext; intros A1; apply set_ext_equiv; split; intros x3 Hx3.
 induction Hx3 as [x1 Hx1]; easy.