Move stuff around.

Shorten some proofs.
Add and prove f_inv_id_{l,r}.

FEM/Compl/Function_compl.v

@@ -530,9 +530,15 @@ Definition f_inv : T2 -> T1 := proj1_sig f_inv_EX.
 Lemma f_inv_correct_l : cancel f f_inv.
 Proof. apply (proj2_sig f_inv_EX). Qed.
 
+Lemma f_inv_id_l : f_inv \o f = id.
+Proof. apply can_equiv, f_inv_correct_l. Qed.
+
 Lemma f_inv_correct_r : cancel f_inv f.
 Proof. apply (proj2_sig f_inv_EX). Qed.
 
+Lemma f_inv_id_r : f \o f_inv = id.
+Proof. apply can_equiv, f_inv_correct_r. Qed.
+
 End Inverse_Def.
 
 
@@ -543,15 +549,10 @@ Context {f : T1 -> T2}.
 Hypothesis Hf : bijective f.
 
 Lemma f_inv_uniq_l : forall (g : T2 -> T1), cancel f g -> g = f_inv Hf.
-Proof.
-intros; apply fun_ext, (bij_can_eq Hf); [easy | apply f_inv_correct_l].
-Qed.
+Proof. move=>> H; apply (bij_can_uniq_r Hf H), f_inv_correct_l. Qed.
 
 Lemma f_inv_uniq_r : forall (g : T2 -> T1), cancel g f -> g = f_inv Hf.
-Proof.
-move=>> Hg; apply: (inj_can_uniq_l _ Hg);
-    [apply bij_inj; easy | apply f_inv_correct_r].
-Qed.
+Proof. move=>> H; apply (bij_can_uniq_l Hf H), f_inv_correct_r. Qed.
 
 Lemma f_inv_bij : bijective (f_inv Hf).
 Proof. apply (bij_can_bij Hf), f_inv_correct_l. Qed.
@@ -578,8 +579,12 @@ End Inverse_Facts1.
 Section Inverse_Facts2.
 
 Context {T1 T2 : Type}.
-Context {f : T1 -> T2}.
+Context {f g : T1 -> T2}.
 Hypothesis Hf : bijective f.
+Hypothesis Hg : bijective g.
+
+Lemma f_inv_ext : same_fun f g -> f_inv Hf = f_inv Hg.
+Proof. move=> /fun_ext_equiv H; subst; f_equal; apply proof_irrel. Qed.
 
 Lemma f_inv_invol : forall (Hf1 : bijective (f_inv Hf)), f_inv Hf1 = f.
 Proof. intros; apply eq_sym, f_inv_uniq_l, f_inv_correct_r. Qed.
@@ -587,12 +592,6 @@ Proof. intros; apply eq_sym, f_inv_uniq_l, f_inv_correct_r. Qed.
 Lemma f_inv_invol_alt : f_inv (f_inv_bij Hf) = f.
 Proof. apply f_inv_invol. Qed.
 
-Context {g : T1 -> T2}.
-Hypothesis Hg : bijective g.
-
-Lemma f_inv_ext : same_fun f g -> f_inv Hf = f_inv Hg.
-Proof. move=> /fun_ext_equiv H; subst; f_equal; apply proof_irrel. Qed.
-
 End Inverse_Facts2.