diff --git a/FEM/Compl/Function_compl.v b/FEM/Compl/Function_compl.v
index 04348d6b6e616dd2938f35588daaecb7a5d289e7..50aa3bdaa0beb36a5613c09400110757b1e68f2a 100644
--- a/FEM/Compl/Function_compl.v
+++ b/FEM/Compl/Function_compl.v
@@ -120,25 +120,19 @@ Proof. intros [x1] HT2 [h]; contradict HT2; apply (inhabits (h x1)). Qed.
 End Inhabited_Facts.
 
 
-Section Swap_Def.
+Section Image_preimage_Facts0.
 
-Context {T1 T2 T3 : Type}.
-Variable f : T1 -> T2 -> T3.
-
-Definition swap : T2 -> T1 -> T3 := fun x2 x1 => f x1 x2.
-
-End Swap_Def.
-
-
-Section Swap_Facts.
+Context {T1 T2 : Type}.
 
-Context {T1 T2 T3 : Type}.
-Variable f : T1 -> T2 -> T3.
+Variable f : T1 -> T2.
 
-Lemma swap_invol : swap (swap f) = f.
-Proof. easy. Qed.
+Lemma im_dec : forall x2, { x1 | f x1 = x2 } + { forall x1, f x1 <> x2 }.
+Proof.
+intros x2; destruct (in_dec (fun x2 => exists x1, f x1 = x2) x2) as [H1 | H1];
+    [left; apply ex_EX | right; apply not_ex_all_not]; easy.
+Qed.
 
-End Swap_Facts.
+End Image_preimage_Facts0.
 
 
 Section Image_preimage_Facts1.
@@ -202,145 +196,116 @@ Qed.
 End Image_preimage_Facts3.
 
 
-Section Range_Def.
+Section Comp_Facts1.
 
-Context {T1 T2 : Type}.
+Context {T1 T2 T3 T4 : Type}.
 Variable f : T1 -> T2.
+Variable g : T2 -> T3.
+Variable h : T3 -> T4.
 
-Definition Rg : T2 -> Prop := image f fullset.
+Lemma comp_correct : forall x1, (g \o f) x1 = g (f x1).
+Proof. easy. Qed.
 
-(* There is an alternate form: "forall x2, exists x1, x2 = f x1", but we choose
- the one compatible with cancel, eg. when "x1" is "g x2" for some "g".
- Note that one can rewrite "x2" with both. *)
-Definition surjective : Prop := forall x2, exists x1, f x1 = x2.
+Lemma comp_assoc : h \o (g \o f) = (h \o g) \o f.
+Proof. easy. Qed.
 
-End Range_Def.
+End Comp_Facts1.
 
 
-Section Range_Facts1.
+Section Comp_Facts2.
 
 Context {T1 T2 : Type}.
-Context {f : T1 -> T2}.
+Variable f : T1 -> T2.
 
-Lemma Rg_correct : forall {x2} x1, f x1 = x2 -> Rg f x2.
-Proof. move=> x2 x1 <-; easy. Qed.
+Lemma comp_id_l : id \o f = f.
+Proof. easy. Qed.
 
-Lemma Rg_ex : forall {x2}, Rg f x2 <-> exists x1, f x1 = x2.
-Proof. intros; split; [intros [x1 _]; exists x1 | move=> [x1 <-]]; easy. Qed.
+Lemma comp_id_r : f \o id = f.
+Proof. easy. Qed.
 
-Lemma Rg_compl : forall {x2}, ~ Rg f x2 <-> forall x1, f x1 <> x2.
-Proof. intros; rewrite -iff_not_r_equiv not_all_not_ex_equiv; apply Rg_ex. Qed.
+Lemma comp_id : forall {T : Type}, id \o id = (id : T -> T).
+Proof. easy. Qed.
 
-Lemma Rg_full_equiv : Rg f = fullset <-> incl fullset (Rg f).
-Proof. split; intros Hf; [rewrite Hf | apply subset_ext_equiv]; easy. Qed.
+End Comp_Facts2.
 
-Lemma surj_correct : incl fullset (Rg f) -> surjective f.
-Proof. intros Hf y; destruct (Hf y) as [x Hx]; [| exists x]; easy. Qed.
 
-Lemma surj_rev : surjective f -> Rg f = fullset.
-Proof.
-intros Hf; apply incl_antisym; intros x2 _;
-    [| destruct (Hf x2) as [x1 Hx1]; apply (Rg_correct x1)]; easy.
-Qed.
-
-Lemma surj_equiv : surjective f <-> Rg f = fullset.
-Proof.
-split; [apply surj_rev | intros Hf; apply surj_correct; rewrite Hf]; easy.
-Qed.
+Section Comp_Facts3.
 
-Lemma surj_equiv_alt : surjective f <-> incl fullset (Rg f).
-Proof. rewrite surj_equiv; apply Rg_full_equiv. Qed.
+Context {T1 T2 T3 : Type}.
+Context {f : T2 -> T3}.
+Hypothesis Hf : injective f.
 
-Lemma surj_can_uniq_r :
-  forall {g h : T2 -> T1}, surjective f -> cancel f g -> cancel f h -> g = h.
-Proof.
-intros g h Hf Hg Hh; apply fun_ext; intros x2.
-destruct (Hf x2) as [x1 <-]; rewrite Hh; auto.
-Qed.
+Lemma comp_inj_r : forall {g h : T1 -> T2}, f \o g = f \o h -> g = h.
+Proof. move=>> /fun_ext_rev H; apply fun_ext; intro; apply Hf, H. Qed.
 
-End Range_Facts1.
+End Comp_Facts3.
 
 
-Section Range_Facts2.
+Section Fun_Def.
 
 Context {T1 T2 T3 : Type}.
-Context {f : T1 -> T2}.
-Context {g : T2 -> T3}.
 
-Lemma preimage_Rg : preimage f (Rg f) = fullset.
-Proof. apply preimage_of_image_full. Qed.
+Definition swap (f : T1 -> T2 -> T3) : T2 -> T1 -> T3 := fun x2 x1 => f x1 x2.
 
-Lemma Rg_comp : Rg (g \o f) = image g (Rg f).
-Proof.
-apply subset_ext_equiv; split; [intros _ [x2 _]; easy |].
-intros _ [_ [x1 _]]; apply: Im; easy.
-Qed.
+Definition Rg (f : T1 -> T2) : T2 -> Prop := image f fullset.
 
-End Range_Facts2.
+(* There is an alternate form: "forall x2, exists x1, x2 = f x1", but we choose
+ the one compatible with cancel, eg. when "x1" is "g x2" for some "g".
+ Note that one can rewrite "x2" with both. *)
+Definition surjective (f : T1 -> T2) : Prop := forall x2, exists x1, f x1 = x2.
 
+End Fun_Def.
 
-Section Comp_Facts1.
 
-Context {T1 T2 T3 T4 : Type}.
-Variable f : T1 -> T2.
-Variable g : T2 -> T3.
-Variable h : T3 -> T4.
+Section Swap_Facts.
 
-Lemma comp_correct : forall x1, (g \o f) x1 = g (f x1).
-Proof. easy. Qed.
+Context {T1 T2 T3 : Type}.
+Variable f : T1 -> T2 -> T3.
 
-Lemma comp_assoc : h \o (g \o f) = (h \o g) \o f.
+Lemma swap_invol : swap (swap f) = f.
 Proof. easy. Qed.
 
-End Comp_Facts1.
+End Swap_Facts.
 
 
-Section Comp_Facts2.
+Section Range_Facts.
 
-Context {T1 T2 : Type}.
+Context {T1 T2 T3 : Type}.
 Context {f : T1 -> T2}.
-Context {g : T2 -> T1}.
-
-Lemma cancel_id : cancel f g <-> g \o f = id.
-Proof. apply iff_sym, fun_ext_equiv. Qed.
-
-Lemma can_surj : cancel g f -> surjective f.
-Proof. intros H x1; exists (g x1); easy. Qed.
-
-End Comp_Facts2.
-
-
-Section Comp_Facts3.
-
-Context {T1 T2 : Type}.
-Variable f : T1 -> T2.
-
-Lemma comp_id_l : id \o f = f.
-Proof. easy. Qed.
+Context {g : T2 -> T3}.
 
-Lemma comp_id_r : f \o id = f.
-Proof. easy. Qed.
+Lemma Rg_correct : forall {x2} x1, f x1 = x2 -> Rg f x2.
+Proof. move=> x2 x1 <-; easy. Qed.
 
-End Comp_Facts3.
+Lemma Rg_ex : forall {x2}, Rg f x2 <-> exists x1, f x1 = x2.
+Proof. intros; split; [intros [x1 _]; exists x1 | move=> [x1 <-]]; easy. Qed.
 
+Lemma Rg_compl : forall {x2}, ~ Rg f x2 <-> forall x1, f x1 <> x2.
+Proof. intros; rewrite -iff_not_r_equiv not_all_not_ex_equiv; apply Rg_ex. Qed.
 
-Section Comp_Facts4.
+Lemma Rg_full_equiv : Rg f = fullset <-> incl fullset (Rg f).
+Proof. split; intros Hf; [rewrite Hf | apply subset_ext_equiv]; easy. Qed.
 
-Context {T1 T2 T3 : Type}.
-Context {f : T2 -> T3}.
-Hypothesis Hf : injective f.
+Lemma preimage_Rg : preimage f (Rg f) = fullset.
+Proof. apply preimage_of_image_full. Qed.
 
-Lemma comp_inj_r : forall {g h : T1 -> T2}, f \o g = f \o h -> g = h.
-Proof. move=>> /fun_ext_rev H; apply fun_ext; intro; apply Hf, H. Qed.
+Lemma Rg_comp : Rg (g \o f) = image g (Rg f).
+Proof.
+apply subset_ext_equiv; split; [intros _ [x2 _]; easy |].
+intros _ [_ [x1 _]]; apply: Im; easy.
+Qed.
 
-End Comp_Facts4.
+End Range_Facts.
 
 
-Section Injective_Facts.
+Section Inj_Facts.
 
 Context {T1 T2 : Type}.
 Context {f : T1 -> T2}.
 
+Lemma fun_from_empty_is_inj : ~ inhabited T1 -> injective f.
+Proof. move=>> HT1 x1; contradict HT1; easy. Qed.
+
 Lemma inj_contra : injective f -> forall x1 y1, x1 <> y1 -> f x1 <> f y1.
 Proof. intros Hf x1 y1; rewrite -contra_equiv; apply Hf. Qed.
 
@@ -354,43 +319,91 @@ Proof. split; [apply inj_contra | apply inj_contra_rev]. Qed.
 Lemma inj_equiv : injective f -> forall x1 y1, f x1 = f y1 <-> x1 = y1.
 Proof. intros Hf x1 y1; split; [apply Hf | apply f_equal]. Qed.
 
-End Injective_Facts.
+Lemma inj_has_left_inv : inhabited T1 -> injective f <-> exists g, cancel f g.
+Proof.
+intros [a1]; split; [intros Hf | intros [g Hg]; apply: can_inj Hg].
+exists (fun x2 => match im_dec f x2 with
+  | inleft H1 => proj1_sig H1
+  | inright _ => a1
+  end).
+intros x1; destruct (im_dec f (f x1)) as [[y1 Hy1] | H1];
+    [apply Hf | contradict H1; rewrite not_all_not_ex_equiv; exists x1]; easy.
+Qed.
+
+End Inj_Facts.
 
 
-Section Inj_surj_bij_Facts1.
+Section Surj_Facts.
 
 Context {T1 T2 : Type}.
+Context {f : T1 -> T2}.
 
-Lemma fun_from_empty_is_inj :
-  forall (f : T1 -> T2), ~ inhabited T1 -> injective f.
-Proof. move=>> HT1 x1; contradict HT1; easy. Qed.
+Lemma surj_correct : incl fullset (Rg f) -> surjective f.
+Proof. intros Hf y; destruct (Hf y) as [x Hx]; [| exists x]; easy. Qed.
+
+Lemma surj_rev : surjective f -> Rg f = fullset.
+Proof.
+intros Hf; apply incl_antisym; intros x2 _;
+    [| destruct (Hf x2) as [x1 Hx1]; apply (Rg_correct x1)]; easy.
+Qed.
 
-Lemma im_dec :
-  forall (f : T1 -> T2) x2, { x1 | f x1 = x2 } + { forall x1, f x1 <> x2 }.
+Lemma surj_equiv : surjective f <-> Rg f = fullset.
 Proof.
-intros f x2; destruct (in_dec (fun x2 => exists x1, f x1 = x2) x2) as [H1 | H1];
-    [left; apply ex_EX | right; apply not_ex_all_not]; easy.
+split; [apply surj_rev | intros Hf; apply surj_correct; rewrite Hf]; easy.
 Qed.
 
-Lemma inj_has_left_inv :
-  forall {f : T1 -> T2}, inhabited T1 -> injective f <-> exists g, cancel f g.
+Lemma surj_equiv_alt : surjective f <-> incl fullset (Rg f).
+Proof. rewrite surj_equiv; apply Rg_full_equiv. Qed.
+
+Lemma surj_id : forall {T : Type}, surjective (id : T -> T).
+Proof. intros T x; exists x; easy. Qed.
+
+End Surj_Facts.
+
+
+Section Can_Facts1.
+
+Context {T1 T2 : Type}.
+Context {f : T1 -> T2}.
+Context {g : T2 -> T1}.
+
+Lemma can_equiv : cancel f g <-> g \o f = id.
+Proof. apply iff_sym, fun_ext_equiv. Qed.
+
+Lemma can_surj : cancel g f -> surjective f.
+Proof. intros H x1; exists (g x1); easy. Qed.
+
+Lemma can_id : forall {T : Type}, cancel (id : T -> T) id.
+Proof. easy. Qed.
+
+End Can_Facts1.
+
+
+Section Can_Facts2.
+
+Context {T1 T2 : Type}.
+Context {f : T1 -> T2}.
+
+Lemma surj_can_uniq_r :
+  forall {g h : T2 -> T1}, surjective f -> cancel f g -> cancel f h -> g = h.
 Proof.
-intros f [a1]; split; [intros Hf | intros [g Hg]; apply: can_inj Hg].
-exists (fun x2 => match im_dec f x2 with
-  | inleft H1 => proj1_sig H1
-  | inright _ => a1
-  end).
-intros x1; destruct (im_dec f (f x1)) as [[y1 Hy1] | H1];
-    [apply Hf | contradict H1; rewrite not_all_not_ex_equiv; exists x1]; easy.
+intros g h Hf Hg Hh; apply fun_ext; intros x2.
+destruct (Hf x2) as [x1 <-]; rewrite Hh; auto.
 Qed.
 
-Lemma surj_has_right_inv :
-  forall {f : T1 -> T2}, surjective f <-> exists g, cancel g f.
+Lemma surj_has_right_inv : surjective f <-> exists g, cancel g f.
 Proof.
-intros; apply iff_sym; split; [intros [g Hg]; eapply can_surj, Hg |].
+apply iff_sym; split; [intros [g Hg]; apply: can_surj Hg |].
 intros Hf; destruct (choice _ Hf) as [g Hg]; exists g; easy.
 Qed.
 
+End Can_Facts2.
+
+
+Section Bij_Facts.
+
+Context {T1 T2 : Type}.
+
 Lemma bij_surj : forall (f : T1 -> T2), bijective f -> surjective f.
 Proof. intros f [g _ H] x2; exists (g x2); rewrite H; easy. Qed.
 
@@ -416,20 +429,10 @@ intros x1 y1 H1; destruct (Hf (f x1)) as [x2 [Hx2a Hx2b]].
 rewrite -(Hx2b x1); [apply Hx2b, eq_sym |]; easy.
 Qed.
 
-End Inj_surj_bij_Facts1.
-
-
-Section Inj_surj_bij_Facts2.
-
-Context {T : Type}.
-
-Lemma surj_id : surjective (@id T).
-Proof. intros x; exists x; easy. Qed.
-
-Lemma bij_id : bijective (@id T).
-Proof. apply bij_equiv; split; [apply inj_id | apply surj_id]. Qed.
+Lemma bij_id : forall {T : Type}, bijective (id : T -> T).
+Proof. intros; apply (Bijective can_id); easy. Qed.
 
-End Inj_surj_bij_Facts2.
+End Bij_Facts.
 
 
 Section Inverse_Def.