Move stiff around.

FEM/Compl/Function_compl.v

@@ -123,7 +123,6 @@ End Inhabited_Facts.
 Section Image_preimage_Facts0.
 
 Context {T1 T2 : Type}.
-
 Variable f : T1 -> T2.
 
 Lemma im_dec : forall x2, { x1 | f x1 = x2 } + { forall x1, f x1 <> x2 }.
@@ -232,11 +231,12 @@ End Comp_Facts2.
 Section Comp_Facts3.
 
 Context {T1 T2 T3 : Type}.
+Context {g h : T1 -> T2}.
 Context {f : T2 -> T3}.
 Hypothesis Hf : injective f.
 
-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 comp_inj_r : f \o g = f \o h -> g = h.
+Proof. move=> /fun_ext_rev H; apply fun_ext; intro; apply Hf, H. Qed.
 
 End Comp_Facts3.
 
@@ -276,12 +276,12 @@ Context {f : T1 -> T2}.
 Lemma Rg_correct : forall {x2} x1, f x1 = x2 -> Rg f x2.
 Proof. move=> x2 x1 <-; 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 Rg_ext : forall (g : T1 -> T2), same_fun f g -> Rg f = Rg g.
 Proof. move=> g /fun_ext ->; 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 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.
 
@@ -305,8 +305,12 @@ Section Inj_Facts.
 Context {T1 T2 T3 : 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_ext :
+  forall {g : T1 -> T2}, same_fun f g -> injective f -> injective g.
+Proof. move=>> H Hf; apply (eq_inj Hf H). 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.
 
 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.
@@ -318,13 +322,6 @@ Lemma inj_contra_equiv :
   injective f <-> forall x1 y1, x1 <> y1 -> f x1 <> f y1.
 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.
-
-Lemma inj_ext :
-  forall {g : T1 -> T2}, same_fun f g -> injective f -> injective g.
-Proof. move=>> H Hf; apply (eq_inj Hf H). Qed.
-
 Lemma inj_comp_compat :
   forall {g : T2 -> T3}, injective f -> injective g -> injective (g \o f).
 Proof. intros; apply inj_comp; easy. Qed.
@@ -332,6 +329,9 @@ Proof. intros; apply inj_comp; easy. Qed.
 Lemma inj_comp_reg : forall (g : T2 -> T3), injective (g \o f) -> injective f.
 Proof. intros g H; apply (inj_compr H). Qed.
 
+Lemma fun_from_empty_is_inj : ~ inhabited T1 -> injective f.
+Proof. move=>> HT1 x1; contradict HT1; easy. Qed.
+
 End Inj_Facts.
 
 
@@ -384,7 +384,6 @@ End Surj_Facts.
 Section Can_Facts1.
 
 Context {T1 T2 : Type}.
-
 Context {f f' : T1 -> T2}.
 Context {g g' : T2 -> T1}.
 
@@ -400,7 +399,6 @@ End Can_Facts1.
 Section Can_Facts2.
 
 Context {T1 T2 : Type}.
-
 Context {f f' : T1 -> T2}.
 Context {g g' : T2 -> T1}.
 
@@ -467,9 +465,12 @@ End Can_Facts4.
 Section Bij_Facts.
 
 Context {T1 T2 T3 : Type}.
-
 Context {f : T1 -> T2}.
 
+Lemma bij_ext :
+  forall {g : T1 -> T2}, same_fun f g -> bijective f -> bijective g.
+Proof. move=>> H Hf; apply (eq_bij Hf H). Qed.
+
 Lemma bij_surj : bijective f -> surjective f.
 Proof. intros [g _ H] x2; exists (g x2); rewrite H; easy. Qed.
 
@@ -497,10 +498,6 @@ Qed.
 Lemma bij_ex_uniq_equiv : bijective f <-> forall x2, exists! x1, f x1 = x2.
 Proof. split; [apply bij_ex_uniq | apply bij_ex_uniq_rev]. Qed.
 
-Lemma bij_ext :
-  forall {g : T1 -> T2}, same_fun f g -> bijective f -> bijective g.
-Proof. move=>> H Hf; apply (eq_bij Hf H). Qed.
-
 Lemma bij_comp_compat :
   forall {g : T2 -> T3}, bijective f -> bijective g -> bijective (g \o f).
 Proof. intros; apply bij_comp; easy. Qed.