diff --git a/Algebra/AffineSpace/AffineSpace_aff_map.v b/Algebra/AffineSpace/AffineSpace_aff_map.v
index 3c82d5e63642a5aabc9556c258d74d7d97df7037..2687b09d7124a1b52c0fdb0cbf506528ec032228 100644
--- a/Algebra/AffineSpace/AffineSpace_aff_map.v
+++ b/Algebra/AffineSpace/AffineSpace_aff_map.v
@@ -469,7 +469,7 @@ Lemma am_gather_equiv :
     aff_map (gather f) <-> (forall i, aff_map (f i)).
 Proof.
 intros n f; pose (O1 := point_of_as E1).
-rewrite (am_lm_equiv O1) fct_lm_gather -lm_gather_equiv.
+rewrite (am_lm_equiv O1) fct_lm_gather lm_gather_equiv.
 apply equiv_forall; intro; rewrite am_lm_equiv; easy.
 Qed.
 
diff --git a/Algebra/ModuleSpace/ModuleSpace_R_compl.v b/Algebra/ModuleSpace/ModuleSpace_R_compl.v
index 81dd5fe5fd885fdab70444882972117346ae4cca..c52299cdccb486c8dff83d4ad252fe0893f48bc9 100644
--- a/Algebra/ModuleSpace/ModuleSpace_R_compl.v
+++ b/Algebra/ModuleSpace/ModuleSpace_R_compl.v
@@ -622,7 +622,7 @@ Lemma part1F_fct_lm :
   forall {n} (i0 : 'I_n.+1),
     lin_map (part1F^~ i0 - (fun=> part1F 0 i0) : 'R^n -> 'R^n.+1).
 Proof.
-intros n i0; apply lm_scatter; intros i; split.
+intros n i0; apply lm_scatter_rev; intros i; split.
 (* *)
 intros u v; rewrite !scatter_eq !fct_minus_eq;
     destruct (ord_eq_dec i i0) as [-> | Hi].
diff --git a/Algebra/ModuleSpace/ModuleSpace_lin_map.v b/Algebra/ModuleSpace/ModuleSpace_lin_map.v
index 83a76440be52798620a7a56bf988cbb9546c0cef..c57f949f726cd20e203a4e0cb7a19ff48ad2e782 100644
--- a/Algebra/ModuleSpace/ModuleSpace_lin_map.v
+++ b/Algebra/ModuleSpace/ModuleSpace_lin_map.v
@@ -401,23 +401,23 @@ Qed.
 
 Lemma lm_gather_equiv :
   forall {n} (f : '(E1 -> E2)^n),
-    (forall i, lin_map (f i)) <-> lin_map (gather f).
-Proof. intros; split; [apply lm_gather | apply lm_gather_rev]. Qed.
+    lin_map (gather f) <-> (forall i, lin_map (f i)).
+Proof. intros; split; [apply lm_gather_rev | apply lm_gather]. Qed.
 
 Lemma lm_scatter :
   forall {n} (f : E1 -> 'E2^n),
-    (forall i, lin_map (scatter f i)) -> lin_map f.
-Proof. intros n f; apply (lm_gather (scatter f)). Qed.
+    lin_map f -> forall i, lin_map (scatter f i).
+Proof. intros n f; apply (lm_gather_rev (scatter f)). Qed.
 
 Lemma lm_scatter_rev :
   forall {n} (f : E1 -> 'E2^n),
-    lin_map f -> forall i, lin_map (scatter f i).
-Proof. intros n f; apply (lm_gather_rev (scatter f)). Qed.
+    (forall i, lin_map (scatter f i)) -> lin_map f.
+Proof. intros n f; apply (lm_gather (scatter f)). Qed.
 
 Lemma lm_scatter_equiv :
   forall {n} (f : E1 -> 'E2^n),
     (forall i, lin_map (scatter f i)) <-> lin_map f.
-Proof. intros n f; apply (lm_gather_equiv (scatter f)). Qed.
+Proof. intros n f; rewrite (lm_gather_equiv (scatter f)); easy. Qed.
 
 End Lin_map_Swap_Facts.