Function_compl:

Add and prove bij_ex_uniq{,_rev}.
Simplify proof of bij_ex_uniq_equiv.

AffineSpace:
Simplify proofs using bij_ex_uniq_equiv.

FEM/Algebra/AffineSpace.v

@@ -122,7 +122,7 @@ Lemma vect_l_bij_ex : forall (A : E) u, exists! B, A --> B = u.
 Proof. apply AffineSpace.ax2. Qed.
 
 Lemma vect_l_bij : forall (A : E), bijective (vect A).
-Proof. intros; apply bij_ex_uniq_equiv, vect_l_bij_ex. Qed.
+Proof. intros; apply bij_ex_uniq_rev, vect_l_bij_ex. Qed.
 
 Lemma vect_zero : forall (A : E), A --> A = 0.
 Proof.
@@ -152,7 +152,7 @@ move=> A' /opp_eq; rewrite -vect_sym; apply HA2.
 Qed.
 
 Lemma vect_r_bij : forall (B : E), bijective (vect^~ B).
-Proof. intros; apply bij_ex_uniq_equiv, vect_r_bij_ex. Qed.
+Proof. intros; apply bij_ex_uniq_rev, vect_r_bij_ex. Qed.
 
 Lemma vect_l_eq : forall (A B1 B2 : E), B1 = B2 -> A --> B1 = A --> B2.
 Proof. intros; subst; easy. Qed.
@@ -298,7 +298,7 @@ intros A; apply (bij_can_bij (vect_l_bij A)); apply transl_correct_l.
 Qed.
 
 Lemma transl_l_bij_ex : forall (A B : E), exists! u, A +++ u = B.
-Proof. intros A; rewrite -bij_ex_uniq_equiv; apply transl_l_bij. Qed.
+Proof. intros; apply bij_ex_uniq, transl_l_bij. Qed.
 
 Lemma transl_r_bij_ex : forall u (B : E), exists! A, A +++ u = B.
 Proof.
@@ -308,7 +308,7 @@ intros A; rewrite transl_opp_equiv; easy.
 Qed.
 
 Lemma transl_r_bij : forall u, bijective (transl^~ u : E -> E).
-Proof. intros; apply bij_ex_uniq_equiv, transl_r_bij_ex. Qed.
+Proof. intros; apply bij_ex_uniq_rev, transl_r_bij_ex. Qed.
 
 Lemma vect_transl : forall (O : E) u v, (O +++ u) --> (O +++ v) = v - u.
 Proof.
@@ -660,7 +660,7 @@ apply (vect_l_inj O); rewrite mapF_correct -vectF_correct HB; easy.
 Qed.
 
 Lemma vectF_l_bij : forall {n} (O : E), bijective (@vectF _ _ _ n O).
-Proof. intros; apply bij_ex_uniq_equiv, vectF_l_bij_ex. Qed.
+Proof. intros; apply bij_ex_uniq_rev, vectF_l_bij_ex. Qed.
 
 Lemma vectF_zero : forall {n} (O : E), vectF O (constF n O) = 0.
 Proof. intros; apply extF; intro; apply vect_zero. Qed.
@@ -878,7 +878,7 @@ intros n O; apply (bij_can_bij (vectF_l_bij O)); apply translF_vectF.
 Qed.
 
 Lemma translF_l_bij_ex : forall {n} O (A : 'E^n), exists! u, translF O u = A.
-Proof. intros n O; rewrite -bij_ex_uniq_equiv; apply translF_l_bij. Qed.
+Proof. intros; apply bij_ex_uniq, translF_l_bij. Qed.
 
 Lemma translF_inj_equiv :
   forall {n} (O : E) (u : 'V^n), injective (translF O u) <-> injective u.

FEM/Compl/Function_compl.v

@@ -480,19 +480,23 @@ intros [Hf1 Hf2]; destruct (choice _ Hf2) as [g Hg];
     apply: (Bijective _ Hg); intro; auto.
 Qed.
 
-Lemma bij_ex_uniq_equiv : bijective f <-> forall x2, exists! x1, f x1 = x2.
+Lemma bij_ex_uniq : bijective f -> forall x2, exists! x1, f x1 = x2.
+Proof.
+rewrite bij_equiv; intros [Hf1 Hf2] x2; destruct (Hf2 x2) as [x1 Hx1];
+    exists x1; split; [| intros y1 Hy1; apply Hf1; rewrite Hy1]; easy.
+Qed.
+
+Lemma bij_ex_uniq_rev : (forall x2, exists! x1, f x1 = x2) -> bijective f.
 Proof.
-rewrite bij_equiv; split.
-(* *)
-intros [Hf1 Hf2] x2; destruct (Hf2 x2) as [x1 Hx1]; exists x1; split; [easy |].
-intros y1 Hy1; apply Hf1; rewrite Hy1; easy.
-(* *)
-intros Hf; split;
+rewrite bij_equiv; intros Hf; split;
     [| intros x2; destruct (Hf x2) as [x1 [Hx1 _]]; exists x1; easy].
 intros x1 y1 H1; destruct (Hf (f x1)) as [x2 [Hx2a Hx2b]].
 rewrite -(Hx2b x1); [apply Hx2b, eq_sym |]; easy.
 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.