Compare revisions

François Clément · François Clément · François Clément · 5ba16a8b · 5ba16a8b · 5ba16a8b
--- a/Algebra/AffineSpace/AffineSpace_FF.v
+++ b/Algebra/AffineSpace/AffineSpace_FF.v
@@ -30,7 +30,7 @@ COPYING file for more details.
 - [vectF O A] is the [n]-family of [V] with [i]-th item [vect O (A i)];
 - [translF O u] is the [n]-family of [E] with [i]-th item [transl O (u i)];
 - [frameF B i0] is the [n]-family [vectF (B i0) (skipF B i0)];
- - [inv_frameF O u i0] is the [n]-family [translF O (insertF i0 0 u)].
+ - [inv_frameF O i0 u] is the [n]-family [translF O (insert0F i0 u)].

 * Used logic axioms

@@ -67,9 +67,9 @@ Context {E : AffineSpace V}.
 Definition vectF {n} O (A : 'E^n) : 'V^n := mapF (vect O) A.
 Definition translF {n} O (u : 'V^n) : 'E^n := mapF (transl O) u.

-Definition frameF {n} (A : 'E^n.+1) i0 : 'V^n := vectF (A i0) (skipF i0 A).
-Definition inv_frameF {n} O (u : 'V^n) i0 : 'E^n.+1 :=
-  translF O (insertF i0 0 u).
+Definition frameF {n} i0 (A : 'E^n.+1) : 'V^n := vectF (A i0) (skipF i0 A).
+Definition inv_frameF {n} i0 O (u : 'V^n) : 'E^n.+1 :=
+  translF O (insert0F i0 u).

 (** Correctness lemmas. *)

@@ -80,13 +80,13 @@ Lemma translF_correct : forall {n} O (u : 'V^n) i, translF O u i = O +++ u i.
 Proof. easy. Qed.

 Lemma frameF_correct :
-  forall {n} (A : 'E^n.+1) i0 i (H : i <> i0),
-    frameF A i0 (insert_ord H) = A i0 --> A i.
+  forall {n i0 i} (H : i <> i0) (A : 'E^n.+1),
+    frameF i0 A (insert_ord H) = A i0 --> A i.
 Proof. intros; unfold frameF; rewrite vectF_correct skipF_correct; easy. Qed.

 Lemma inv_frameF_correct :
-  forall {n} (O : E) (u : 'V^n) i0 j,
-    inv_frameF O u i0 (skip_ord i0 j) = O +++ u j.
+  forall {n} i0 j (O : E) (u : 'V^n),
+    inv_frameF i0 O u (skip_ord i0 j) = O +++ u j.
 Proof.
 intros; unfold inv_frameF; rewrite translF_correct insertF_correct; easy.
 Qed.
@@ -221,19 +221,19 @@ rewrite !vectF_correct Hi2; easy.
 Qed.

 Lemma vectF_insertF :
-  forall {n} O (A : 'E^n) Ai0 i0,
+  forall {n} O i0 Ai0 (A : 'E^n),
    vectF O (insertF i0 Ai0 A) = insertF i0 (O --> Ai0) (vectF O A).
 Proof.
-intros n O A Ai0 i0; extF i; destruct (ord_eq_dec i i0).
+intros n O i0 Ai0 A; extF i; destruct (ord_eq_dec i i0).
 rewrite vectF_correct !insertF_correct_l; easy.
 rewrite vectF_correct !insertF_correct_r; easy.
 Qed.

 Lemma vectF_skipF :
-  forall {n} O (A : 'E^n.+1) i0,
+  forall {n} O i0 (A : 'E^n.+1),
    vectF O (skipF i0 A) = skipF i0 (vectF O A).
 Proof.
-intros n O A i0; extF j; destruct (lt_dec j i0).
+intros n O i0 A; extF j; destruct (lt_dec j i0).
 rewrite vectF_correct !skipF_correct_l; easy.
 rewrite vectF_correct !skipF_correct_r; easy.
 Qed.
@@ -400,19 +400,19 @@ rewrite !translF_correct Hi2; easy.
 Qed.

 Lemma translF_insertF :
-  forall {n} (O : E) (u : 'V^n) u0 i0,
+  forall {n} (O : E) i0 u0 (u : 'V^n),
    translF O (insertF i0 u0 u) = insertF i0 (O +++ u0) (translF O u).
 Proof.
-intros n O u u0 i0; extF i; destruct (ord_eq_dec i i0).
+intros n O i0 u0 u; extF i; destruct (ord_eq_dec i i0).
 rewrite translF_correct !insertF_correct_l; easy.
 rewrite translF_correct !insertF_correct_r; easy.
 Qed.

 Lemma translF_skipF :
-  forall {n} (O : E) (u : 'V^n.+1) i0,
+  forall {n} (O : E) i0 (u : 'V^n.+1),
    translF O (skipF i0 u) = skipF i0 (translF O u).
 Proof.
-intros n O A i0; extF j; destruct (lt_dec j i0).
+intros n O i0 u; extF j; destruct (lt_dec j i0).
 rewrite translF_correct !skipF_correct_l; easy.
 rewrite translF_correct !skipF_correct_r; easy.
 Qed.
@@ -450,7 +450,7 @@ rewrite translF_correct !concatn_ord_correct; easy.
 Qed.

 Lemma frameF_inv_frameF :
-  forall {n} (O : E) (u : 'V^n) i0, frameF (inv_frameF O u i0) i0 = u.
+  forall {n} i0 (O : E) (u : 'V^n), frameF i0 (inv_frameF i0 O u) = u.
 Proof.
 intros; unfold frameF, inv_frameF; apply eq_sym, translF_vectF_equiv.
 rewrite translF_correct (insertF_correct_l _ _ (erefl _)).
@@ -458,26 +458,26 @@ rewrite -{1}(transl_zero O) translF_insertF skipF_insertF; easy.
 Qed.

 Lemma inv_frameF_frameF :
-  forall {n} (A : 'E^n.+1) i0, inv_frameF (A i0) (frameF A i0) i0 = A.
+  forall {n} i0 (A : 'E^n.+1), inv_frameF i0 (A i0) (frameF i0 A) = A.
 Proof.
 intros; unfold frameF, inv_frameF; apply eq_sym, translF_vectF_equiv.
 rewrite -(vect_zero (A i0)) -vectF_insertF insertF_skipF; easy.
 Qed.

 Lemma frameF_inj_equiv :
-  forall {n} (A : 'E^n.+1) i0,
-    injective (frameF A i0) <-> injective (skipF i0 A).
+  forall {n} i0 (A : 'E^n.+1),
+    injective (frameF i0 A) <-> injective (skipF i0 A).
 Proof. move=>>; apply vectF_inj_equiv. Qed.

 Lemma inv_frameF_inj_equiv :
-  forall {n} (O : E) (u : 'V^n) i0,
-    injective (skipF i0 (inv_frameF O u i0)) <-> injective u.
+  forall {n} i0 (O : E) (u : 'V^n),
+    injective (skipF i0 (inv_frameF i0 O u)) <-> injective u.
 Proof. move=>>; rewrite -frameF_inj_equiv frameF_inv_frameF; easy. Qed.

 (* (preimage (transl (A i0)) PE) will be (vectP PE (A i0)) below *)
 Lemma frameF_inclF :
-  forall {PE : E -> Prop} {n} {A : 'E^n.+1} i0,
-    inclF A PE -> inclF (frameF A i0) (preimage (transl (A i0)) PE).
+  forall {PE : E -> Prop} {n} i0 {A : 'E^n.+1},
+    inclF A PE -> inclF (frameF i0 A) (preimage (transl (A i0)) PE).
 Proof.
 move=>> HA i; unfold preimage, frameF.
 rewrite vectF_correct transl_correct_l.
@@ -486,70 +486,67 @@ apply skipF_monot_l, invalF_refl.
 Qed.

 Lemma frameF_invalF :
-  forall {n1 n2} (A1 : 'E^n1.+1) (A2 : 'E^n2.+1) i1 i2,
+  forall {n1 n2} i1 i2 (A1 : 'E^n1.+1) (A2 : 'E^n2.+1),
    A1 i1 = A2 i2 ->
-    invalF (skipF i1 A1) (skipF i2 A2) -> invalF (frameF A1 i1) (frameF A2 i2).
+    invalF (skipF i1 A1) (skipF i2 A2) -> invalF (frameF i1 A1) (frameF i2 A2).
 Proof. move=>> H; unfold frameF; rewrite H; apply vectF_invalF. Qed.

 Lemma frameF_invalF_rev :
-  forall {n1 n2} (A1 : 'E^n1.+1) (A2 : 'E^n2.+1) i1 i2,
+  forall {n1 n2} i1 i2 (A1 : 'E^n1.+1) (A2 : 'E^n2.+1),
    A1 i1 = A2 i2 ->
-    invalF (frameF A1 i1) (frameF A2 i2) -> invalF (skipF i1 A1) (skipF i2 A2).
+    invalF (frameF i1 A1) (frameF i2 A2) -> invalF (skipF i1 A1) (skipF i2 A2).
 Proof. move=>> H; unfold frameF; rewrite H; apply vectF_invalF. Qed.

 Lemma frameF_invalF_equiv :
-  forall {n1 n2} (A1 : 'E^n1.+1) (A2 : 'E^n2.+1) i1 i2,
+  forall {n1 n2} i1 i2 (A1 : 'E^n1.+1) (A2 : 'E^n2.+1),
    A1 i1 = A2 i2 ->
-    invalF (frameF A1 i1) (frameF A2 i2) <->
+    invalF (frameF i1 A1) (frameF i2 A2) <->
    invalF (skipF i1 A1) (skipF i2 A2).
 Proof. move=>> H; unfold frameF; rewrite H; apply vectF_invalF. Qed.

-Lemma frameF_1 : forall (A : 'E^1), frameF A ord0 = 0.
+Lemma frameF_1 : forall (A : 'E^1), frameF ord0 A = 0.
 Proof. intros; unfold frameF, vectF; apply mapF_nil; easy. Qed.

-Lemma frameF_singleF : forall (A : E), frameF (singleF A) ord0 = 0.
+Lemma frameF_singleF : forall (A : E), frameF ord0 (singleF A) = 0.
 Proof. intros; apply frameF_1. Qed.

 Lemma frameF_2_0 :
-  forall (A : 'E^2), frameF A ord0 ord0 = A ord0 --> A ord_max.
+  forall (A : 'E^2), frameF ord0 A ord0 = A ord0 --> A ord_max.
 Proof.
-intros; rewrite -(frameF_correct _ _ _ ord_max_not_0)
-    insert_ord_max ord_one; easy.
+intros; rewrite -(frameF_correct ord_max_not_0) insert_ord_max ord_one; easy.
 Qed.

 Lemma frameF_2_1 :
-  forall (A : 'E^2), frameF A ord_max ord0 = A ord_max --> A ord0.
-Proof.
-intros; rewrite -(frameF_correct _ _ _ ord_0_not_max) insert_ord_0; easy.
-Qed.
+  forall (A : 'E^2), frameF ord_max A ord0 = A ord_max --> A ord0.
+Proof. intros; rewrite -(frameF_correct ord_0_not_max) insert_ord_0; easy. Qed.

 Lemma frameF_coupleF_0 :
-  forall (A B : E), frameF (coupleF A B) ord0 ord0 = A --> B.
+  forall (A B : E), frameF ord0 (coupleF A B) ord0 = A --> B.
 Proof. intros; rewrite frameF_2_0 coupleF_0 coupleF_1; easy. Qed.

 Lemma frameF_coupleF_1 :
-  forall (A B : E), frameF (coupleF A B) ord_max ord0 = B --> A.
+  forall (A B : E), frameF ord_max (coupleF A B) ord0 = B --> A.
 Proof. intros; rewrite frameF_2_1 coupleF_0 coupleF_1; easy. Qed.

 Lemma frameF_skipF :
-  forall {n} (A : 'E^n.+2) {i0 i1} (H10 : i1 <> i0) (H01 : i0 <> i1),
-    frameF (skipF i0 A) (insert_ord H10) =
-      skipF (insert_ord H01) (frameF A i1).
+  forall {n} {i0 i1} (H10 : i1 <> i0) (H01 : i0 <> i1) (A : 'E^n.+2),
+    frameF (insert_ord H10) (skipF i0 A) =
+      skipF (insert_ord H01) (frameF i1 A).
 Proof.
-intros n A i0 i1 H10 H01; unfold frameF.
+intros n i0 i1 H10 H01 A; unfold frameF.
 rewrite -vectF_skipF (skipF_correct_alt H10); [| apply skip_insert_ord].
 rewrite -skip2F_correct skip2F_equiv_def; easy.
 Qed.

 Lemma frameF_skipF_alt :
-  forall {n} (A : 'E^n.+2) {i0 i1} {H10 : i1 <> i0},
-    frameF (skipF i0 A) (insert_ord H10) =
-      skipF (insert_ord (not_eq_sym H10)) (frameF A i1).
+  forall {n} {i0 i1} {H10 : i1 <> i0} (A : 'E^n.+2),
+    frameF (insert_ord H10) (skipF i0 A) =
+      skipF (insert_ord (not_eq_sym H10)) (frameF i1 A).
 Proof. intros; apply frameF_skipF. Qed.

 Lemma frameF_permutF :
-  forall {n} {A : 'E^n.+1} {i0} {p} (Hp : injective p),
-    frameF (permutF p A) i0 = permutF (skip_f_ord Hp i0) (frameF A (p i0)).
+  forall {n i0 p} (Hp : injective p) {A : 'E^n.+1},
+    frameF i0 (permutF p A) = permutF (skip_f_ord Hp i0) (frameF (p i0) A).
 Proof. intros; unfold frameF; rewrite skipF_permutF; easy. Qed.

 Context {V1 V2 : ModuleSpace K}.
@@ -577,9 +574,9 @@ Lemma fct_translF_eq :
 Proof. intros; extF; rewrite !translF_correct; apply fct_transl_eq. Qed.

 Lemma frameF_mapF :
-  forall {n} {A1 : 'E1^n.+1} {i0} {f : E1 -> E2},
-    frameF (mapF f A1) i0 =
-      mapF (vect (f (A1 i0)) \o f \o transl (A1 i0)) (frameF A1 i0).
+  forall {n i0} {f : E1 -> E2} {A1 : 'E1^n.+1},
+    frameF i0 (mapF f A1) =
+      mapF (vect (f (A1 i0)) \o f \o transl (A1 i0)) (frameF i0 A1).
 Proof.
 intros; unfold frameF; rewrite mapF_correct -mapF_skipF.
 unfold vectF; rewrite -2!mapF_comp {1}comp_assoc -(comp_assoc (vect _)).
@@ -602,16 +599,16 @@ Lemma translF_ms_eq :
 Proof. intros; extF; rewrite translF_correct ms_transl_eq; easy. Qed.

 Lemma frameF_ms_eq :
-  forall {n} (A : 'V^n.+1) i0, frameF A i0 = skipF i0 A - constF n (A i0).
+  forall {n} i0 (A : 'V^n.+1), frameF i0 A = skipF i0 A - constF n (A i0).
 Proof. intros; unfold frameF; rewrite vectF_ms_eq; easy. Qed.

 Lemma inv_frameF_ms_eq :
-  forall {n} (u : 'V^n) (O : V) i0,
-    inv_frameF O u i0 = constF n.+1 O + insertF i0 0 u.
+  forall {n} i0 (O : V) (u : 'V^n),
+    inv_frameF i0 O u = constF n.+1 O + insert0F i0 u.
 Proof. intros; unfold inv_frameF; rewrite translF_ms_eq; easy. Qed.

 Lemma injF_ms_equiv :
-  forall {n} (A : 'V^n.+1), injective A <-> forall i0, ~ inF 0 (frameF A i0).
+  forall {n} (A : 'V^n.+1), injective A <-> forall i0, ~ inF 0 (frameF i0 A).
 Proof.
 intros n A; rewrite injF_g_equiv; split; intros H i0;
    [rewrite frameF_ms_eq | rewrite -frameF_ms_eq]; easy.

--- a/Algebra/AffineSpace/AffineSpace_aff_map.v
+++ b/Algebra/AffineSpace/AffineSpace_aff_map.v
@@ -357,11 +357,11 @@ Context {V : ModuleSpace K}.
 Context {E : AffineSpace V}.

 Lemma insertF_fct_lm :
-  forall {n} x0 i0,
+  forall {n} i0 x0,
    fct_lm (fun A : 'E^n => insertF i0 x0 A) (constF n x0) =
      (fun u : 'V^n => insert0F i0 u).
 Proof.
-intros n x0 i0; unfold fct_lm; fun_ext u; extF i.
+intros n i0 x0; unfold fct_lm; fun_ext u; extF i.
 rewrite fct_vect_eq insertF_constF constF_correct.
 destruct (ord_eq_dec i i0) as [-> | Hi].
 rewrite !insertF_correct_l//; apply vect_zero.
@@ -369,9 +369,9 @@ rewrite !insertF_correct_r fct_transl_eq constF_correct transl_correct_r; easy.
 Qed.

 Lemma insertF_am :
-  forall {n} x0 i0, aff_map (fun A : 'E^n => insertF i0 x0 A).
+  forall {n} i0 x0, aff_map (fun A : 'E^n => insertF i0 x0 A).
 Proof.
-intros n x0 i0; apply (am_lm (constF _ x0)).
+intros n i0 x0; apply (am_lm (constF _ x0)).
 rewrite insertF_fct_lm; apply insert0F_lm.
 Qed.

@@ -777,7 +777,7 @@ End ModuleSpace_AffineSpace_Morphism_R_Facts.
 Section Euclidean_space_AffineSpace_Morphism_Facts.

 Lemma part1F_am :
-  forall {n} (i0 : 'I_n.+1), aff_map_ms (part1F^~ i0 : 'R^n -> 'R^n.+1).
+  forall {n} (i0 : 'I_n.+1), aff_map_ms (part1F i0 : 'R^n -> 'R^n.+1).
 Proof. intros; apply am_lm_0, part1F_fct_lm. Qed.

 End Euclidean_space_AffineSpace_Morphism_Facts.

--- a/Algebra/AffineSpace/AffineSpace_baryc.v
+++ b/Algebra/AffineSpace/AffineSpace_baryc.v
@@ -262,18 +262,18 @@ Proof. intros; f_equal; easy. Qed.

 Lemma isobaryc_correct :
  forall {n} (A : 'E^n),
-    invertible (plusn1 K n) -> aff_comb 1 A (isobarycenter A).
+    invertible (plusn1 n : K) -> aff_comb 1 A (isobarycenter A).
 Proof. intros; apply baryc_correct; easy. Qed.

 Lemma isobaryc_orig :
  forall {n} (A : 'E^n) O,
-    invertible (plusn1 K n) ->
-    scal (plusn1 K n) (O --> isobarycenter A) = sum (vectF O A).
+    invertible (plusn1 n : K) ->
+    scal (plusn1 n) (O --> isobarycenter A) = sum (vectF O A).
 Proof. intros; rewrite -lc_ones_l; apply baryc_orig; easy. Qed.

 Lemma isobaryc_equiv :
  forall {n} (A : 'E^n) G,
-    invertible (plusn1 K n) ->
+    invertible (plusn1 n : K) ->
    G = isobarycenter A <-> aff_comb 1 A G.
 Proof. intros; apply baryc_equiv; easy. Qed.

@@ -362,7 +362,7 @@ Qed.

 Lemma transl_lc :
  forall {n} i0 (A : E) L (u : 'V^n),
-    A +++ lin_comb L u = barycenter (part1F L i0) (insertF i0 A (translF A u)).
+    A +++ lin_comb L u = barycenter (part1F i0 L) (insertF i0 A (translF A u)).
 Proof.
 intros n i0 A L u; apply (baryc_orig_equiv A);
  rewrite sum_insertF_baryc; [apply invertible_one |].
@@ -371,62 +371,62 @@ rewrite vect_zero scal_zero_r plus_zero_l vectF_translF; easy.
 Qed.

 Lemma baryc_insertF :
-  forall {n} i0 O (A : 'E^n) L,
-    barycenter (part1F L i0) (insertF i0 O A) = O +++ lin_comb L (vectF O A).
+  forall {n} i0 O L (A : 'E^n),
+    barycenter (part1F i0 L) (insertF i0 O A) = O +++ lin_comb L (vectF O A).
 Proof. intros; rewrite (transl_lc i0) translF_vectF; easy. Qed.

 Lemma vectF_lc :
-  forall {n} i0 O (A : 'E^n) L,
-    lin_comb L (vectF O A) = O --> barycenter (part1F L i0) (insertF i0 O A).
+  forall {n} i0 O L (A : 'E^n),
+    lin_comb L (vectF O A) = O --> barycenter (part1F i0 L) (insertF i0 O A).
 Proof.
-intros n i0 O A L; apply (transl_l_inj O).
+intros n i0 O L A; apply (transl_l_inj O).
 rewrite -(baryc_insertF i0) transl_correct_l; easy.
 Qed.

 Lemma vectF_lc_skipF :
-  forall {n} i0 (A : 'E^n.+1) L,
+  forall {n} i0 L (A : 'E^n.+1),
    lin_comb L (vectF (A i0) A) =
      lin_comb (skipF i0 L) (vectF (A i0) (skipF i0 A)).
 Proof.
-intros n i0 A L; rewrite (lc_skipF i0) vectF_correct vect_zero
+intros n i0 L A; rewrite (lc_skipF i0) vectF_correct vect_zero
    scal_zero_r plus_zero_l; easy.
 Qed.

 Lemma vectF_lc_0 :
-  forall {n} (A : 'E^n.+1) L,
+  forall {n} L (A : 'E^n.+1),
    lin_comb L (vectF (A ord0) A) =
      lin_comb (liftF_S L) (vectF (A ord0) (liftF_S A)).
 Proof. intros; rewrite -!skipF_first; apply vectF_lc_skipF. Qed.

 Lemma vectF_lc_max :
-  forall {n} (A : 'E^n.+1) L,
+  forall {n} L (A : 'E^n.+1),
    lin_comb L (vectF (A ord_max) A) =
      lin_comb (widenF_S L) (vectF (A ord_max) (widenF_S A)).
 Proof. intros; rewrite -!skipF_last; apply vectF_lc_skipF. Qed.

 Lemma frameF_lc :
-  forall {n} {A : 'E^n.+1} {i0 L}, sum L = 1 ->
-    lin_comb L (frameF A i0) = A i0 --> barycenter (part1F L i0) A.
+  forall {n i0 L} {A : 'E^n.+1}, sum L = 1 ->
+    lin_comb L (frameF i0 A) = A i0 --> barycenter (part1F i0 L) A.
 Proof.
-intros n A i0 L HL; unfold frameF; rewrite (vectF_lc i0) insertF_skipF; easy.
+intros n i0 L A HL; unfold frameF; rewrite (vectF_lc i0) insertF_skipF; easy.
 Qed.

 Lemma baryc_frameF_equiv :
-  forall {n L} (A : 'E^n.+1) G i0, sum L = 1 ->
-    G = barycenter L A <-> A i0 --> G = lin_comb (skipF i0 L) (frameF A i0).
+  forall {n} i0 {L} (A : 'E^n.+1) G, sum L = 1 ->
+    G = barycenter L A <-> A i0 --> G = lin_comb (skipF i0 L) (frameF i0 A).
 Proof.
-intros n L A G i0 HL.
+intros n i0 L A G HL.
 assert (HL0 : invertible (sum L)) by now apply invertible_eq_one.
 rewrite (baryc_orig_equiv (A i0) _ HL0) HL scal_one_l// vectF_lc_skipF//.
 Qed.

 Lemma barycenter2_r :
-  forall {n1 n2} L1 (A1 : 'E^n1) M12 (A2 : 'E^n2),
+  forall {n1 n2} L1 M12 (A1 : 'E^n1) (A2 : 'E^n2),
    invertible (sum L1) -> (forall i1, sum (M12 i1) = 1) ->
    (forall i1, A1 i1 = barycenter (M12 i1) A2) ->
    barycenter L1 A1 = barycenter (fun i2 => lin_comb L1 (M12^~ i2)) A2.
 Proof.
-intros n1 n2 L1 A1 M12 A2 HL1 HM12 HA1; pose (O := point_of_as E).
+intros n1 n2 L1 M12 A1 A2 HL1 HM12 HA1; pose (O := point_of_as E).
 assert (HLM : sum (fun i2 => lin_comb L1 (M12^~ i2)) = sum L1).
  rewrite -lc_sum_r (lc_ext_r 1).
  apply lc_ones_r.
@@ -439,12 +439,12 @@ rewrite -(lc2_l_alt HA1'); apply baryc_orig; easy.
 Qed.

 Lemma barycenter2_r_alt :
-  forall {n1 n2} L1 (A1 : 'E^n1) M12 (A2 : 'E^n2),
+  forall {n1 n2} L1 M12 (A1 : 'E^n1) (A2 : 'E^n2),
    invertible (sum L1) -> (forall i1, sum (M12 i1) = 1) ->
    (forall i1, A1 i1 = barycenter (M12 i1) A2) ->
    barycenter L1 A1 = barycenter (lin_comb L1 M12) A2.
 Proof.
-intros n1 n2 L1 A1 M12 A2 HL1 HM12 H; rewrite (barycenter2_r _ _ M12 A2)//.
+intros n1 n2 L1 M12 A1 A2 HL1 HM12 H; rewrite (barycenter2_r _ M12 _ A2)//.
 f_equal; extF; apply eq_sym, fct_lc_r_eq.
 Qed.

@@ -496,11 +496,11 @@ rewrite lc_3 3!vectF_correct 2!tripleF_0 2!tripleF_1 2!tripleF_2; easy.
 Qed.

 Lemma baryc_skip_zero :
-  forall {n} L (A : 'E^n.+1) i0,
+  forall {n} i0 L (A : 'E^n.+1),
    invertible (sum L) -> L i0 = 0 ->
    barycenter L A = barycenter (skipF i0 L) (skipF i0 A).
 Proof.
-intros n L A i0 HL Hi0; apply baryc_equiv; unfold aff_comb.
+intros n i0 L A HL Hi0; apply baryc_equiv; unfold aff_comb.
 rewrite -(plus_zero_l (sum _)) -Hi0 -sum_skipF; easy.
 rewrite -(plus_zero_l (lin_comb _ _))
    -{1}(scal_zero_l (barycenter L A --> A i0))
@@ -510,25 +510,23 @@ apply baryc_correct; easy.
 Qed.

 Lemma baryc_insert_zero :
-  forall {n} L (A : 'E^n) x0 i0,
+  forall {n} i0 x0 L (A : 'E^n),
    invertible (sum L) ->
-    barycenter L A = barycenter (insertF i0 0 L) (insertF i0 x0 A).
+    barycenter L A = barycenter (insert0F i0 L) (insertF i0 x0 A).
 Proof.
-intros n L A x0 i0 HL; rewrite (baryc_skip_zero (insertF _ _ _) _ i0).
+intros n i0 x0 L A HL; rewrite (baryc_skip_zero i0).
 rewrite !skipF_insertF; easy.
 rewrite sum_insertF plus_zero_l; easy.
 apply insertF_correct_l; easy.
 Qed.

 Lemma baryc_squeezeF :
-  forall {n} {L} {A : 'E^n.+1} {i0 i1},
-    invertible (sum L) -> i1 <> i0 -> A i1 = A i0 ->
+  forall {n} {i0 i1} (H : i1 <> i0) {L} {A : 'E^n.+1},
+    invertible (sum L) -> A i1 = A i0 ->
    barycenter L A = barycenter (squeezeF i0 i1 L) (skipF i1 A).
 Proof.
-intros n L A i0 i1 HL Hia Hib; apply baryc_equiv.
-apply invertible_sum_squeezeF; easy.
-apply ac_squeezeF; try easy.
-apply baryc_correct; easy.
+intros; apply baryc_equiv; [apply invertible_sum_squeezeF; easy |].
+apply ac_squeezeF; [..| apply baryc_correct]; easy.
 Qed.

 Lemma baryc_injF_ex :
@@ -553,7 +551,7 @@ destruct (Hn (squeezeF i0 i1 L) (skipF i1 A)) as [m [M [B [H1 [H2 [H3 H4]]]]]];
    try now apply invertible_sum_squeezeF.
 exists m, M, B; repeat split; try easy.
 apply (skipF_monot_r i1); easy.
-rewrite (baryc_squeezeF _ Hib); easy.
+rewrite (baryc_squeezeF Hib); easy.
 Qed.

 Lemma baryc_filter_n0F :
@@ -578,9 +576,9 @@ destruct (baryc_normalized
 rewrite -invertible_sum_equiv//.
 apply baryc_filter_n0F; easy.
 eexists; exists (scal (/ sum (filter_n0F L)) (filter_n0F L)),
-    (filter_n0F_gen L A); repeat split; try easy.
-2: apply filterPF_invalF.
-intros; rewrite fct_scal_r_eq scal_eq_K. apply mult_not_zero_l.
+    (filter_n0F_gen L A); repeat split;
+    [easy | | apply filterPF_invalF | easy].
+intros; rewrite fct_scal_r_eq scal_eq_K; apply mult_not_zero_l.
 apply inv_invertible; rewrite -invertible_sum_equiv//.
 apply filter_neqF_correct.
 Qed.
@@ -911,14 +909,23 @@ rewrite minus_zero_equiv lc_constF_r HL scal_one; easy.
 Qed.

 Lemma baryc_frameF_ms_eq :
-  forall {n L} {A : 'E^n.+1} i0, sum L = 1 ->
+  forall {n} i0 {L} {A : 'E^n.+1}, sum L = 1 ->
    barycenter_ms L A =
      A i0 + lin_comb (skipF i0 L) (skipF i0 A - constF n (A i0)).
 Proof.
-intros n L A i0 HL; apply eq_sym, (baryc_frameF_equiv A _ i0 HL).
+intros n i0 L A HL; apply eq_sym, (baryc_frameF_equiv i0); [easy |].
 rewrite frameF_ms_eq; apply: minus_plus_l.
 Qed.

+Lemma isobaryc_ms_eq :
+  forall {n} (A : 'E^n), invertible (plusn1 n : K) ->
+    isobarycenter_ms A = scal (/ plusn1 n) (sum A).
+Proof.
+intros n A Hn; rewrite isobaryc_ms_correct; unfold isobarycenter.
+destruct (baryc_normalized 1 A (barycenter 1 A)) as [HL1 ->]; [easy.. |].
+rewrite -baryc_ms_correct baryc_ms_eq// lc_scal_l lc_ones_l; easy.
+Qed.
+
 End ModuleSpace_AffineSpace.



--- a/Algebra/Finite_dim/Finite_dim_AS_aff_basis.v
+++ b/Algebra/Finite_dim/Finite_dim_AS_aff_basis.v
@@ -142,50 +142,50 @@ Lemma has_aff_dim_cas :
 Proof. move=>> [B HB]; apply (aff_basis_cas _ HB). Qed.

 Lemma aff_basis_lin_basis :
-  forall {PE n} {A : 'E^n.+1} O i0,
-    aff_span A O -> basis (vectP PE O) (frameF A i0) -> aff_basis PE A.
+  forall {PE n} i0 O {A : 'E^n.+1},
+    aff_span A O -> basis (vectP PE O) (frameF i0 A) -> aff_basis PE A.
 Proof.
 move=>> HO; apply modus_ponens_and;
    [apply aff_gen_lin_gen; easy | apply aff_indep_lin_indep].
 Qed.

 Lemma aff_basis_lin_basis_rev :
-  forall {PE : E -> Prop} {n} {A : 'E^n.+1} {O} i0,
-    PE O -> aff_basis PE A -> basis (vectP PE O) (frameF A i0).
+  forall {PE : E -> Prop} {n} i0 {O} {A : 'E^n.+1},
+    PE O -> aff_basis PE A -> basis (vectP PE O) (frameF i0 A).
 Proof.
 move=>> HO; apply modus_ponens_and;
    [apply aff_gen_lin_gen_rev; easy | apply aff_indep_lin_indep_rev].
 Qed.

 Lemma aff_basis_lin_basis_equiv :
-  forall {PE n} {A : 'E^n.+1} {O} i0,
+  forall {PE n} i0 {O} {A : 'E^n.+1},
    PE O -> aff_span A O ->
-    aff_basis PE A <-> basis (vectP PE O) (frameF A i0).
+    aff_basis PE A <-> basis (vectP PE O) (frameF i0 A).
 Proof.
 intros; apply and_iff_compat;
    [apply aff_gen_lin_gen_equiv; easy | apply aff_indep_lin_indep_equiv].
 Qed.

 Lemma lin_basis_aff_basis :
-  forall {PV n} {B : 'V^n} (O : E) i0,
+  forall {PV n} i0 (O : E) {B : 'V^n},
    zero_closed PV ->
-    aff_basis (translP PV O) (inv_frameF O B i0) -> basis PV B.
+    aff_basis (translP PV O) (inv_frameF i0 O B) -> basis PV B.
 Proof.
 move=>> HO; apply modus_ponens_and;
    [apply lin_gen_aff_gen; easy | apply lin_indep_aff_indep].
 Qed.

 Lemma lin_basis_aff_basis_rev :
-  forall {PV n} {B : 'V^n} (O : E) i0,
-    basis PV B -> aff_basis (translP PV O) (inv_frameF O B i0).
+  forall {PV n} i0 (O : E) {B : 'V^n},
+    basis PV B -> aff_basis (translP PV O) (inv_frameF i0 O B).
 Proof.
 move=>>; apply modus_ponens_and;
    [apply lin_gen_aff_gen_rev; easy | apply lin_indep_aff_indep_rev].
 Qed.

 Lemma lin_basis_aff_basis_equiv :
-  forall {PV n} {B : 'V^n} (O : E) i0, zero_closed PV ->
-    basis PV B <-> aff_basis (translP PV O) (inv_frameF O B i0).
+  forall {PV n} i0 (O : E) {B : 'V^n}, zero_closed PV ->
+    basis PV B <-> aff_basis (translP PV O) (inv_frameF i0 O B).
 Proof.
 intros; apply and_iff_compat;
    [apply lin_gen_aff_gen_equiv; easy | apply lin_indep_aff_indep_equiv].
@@ -194,7 +194,7 @@ Qed.
 Lemma has_aff_dim_has_dim :
  forall {PE : E -> Prop} {n} O, has_dim (vectP PE O) n -> has_aff_dim PE n.
 Proof.
-move=> PE n O [B /(lin_basis_aff_basis_rev O ord0) HB];
+move=> PE n O [B /(lin_basis_aff_basis_rev ord0 O) HB];
    rewrite translP_vectP in HB; apply (Aff_dim _ _ _ HB).
 Qed.

@@ -225,7 +225,7 @@ Qed.
 Lemma has_dim_has_aff_dim_rev :
  forall {PV n} (O : E), has_dim PV n -> has_aff_dim (translP PV O) n.
 Proof.
-move=> PV n O [B /(lin_basis_aff_basis_rev O ord0) HB];
+move=> PV n O [B /(lin_basis_aff_basis_rev ord0 O) HB];
    apply (Aff_dim _ _ _ HB).
 Qed.

@@ -260,7 +260,7 @@ intros PE n A HPE HA; destruct (has_aff_dim_nonempty HPE) as [O HO].
 assert (HO' : aff_span A O) by now rewrite -HA.
 move: (has_aff_dim_has_dim_rev HO HPE) => HPE'.
 move: (aff_gen_lin_gen_rev ord0 HO HA) => HA'.
-apply (aff_basis_lin_basis _ ord0 HO').
+apply (aff_basis_lin_basis ord0 _ HO').
 apply (lin_gen_basis HPE' HA').
 Qed.

@@ -278,7 +278,7 @@ Lemma aff_indep_aff_gen :
 Proof.
 intros PE n A HPE HA1 HA2.
 move: (has_aff_dim_has_dim_rev (HA1 ord0) HPE) => HPE'.
-apply (aff_gen_lin_gen (A ord0) ord0).
+apply (aff_gen_lin_gen ord0 (A ord0)).
 apply aff_span_inclF_diag.
 apply (lin_indep_lin_gen HPE'); try easy.
 apply frameF_inclF; easy.

--- a/Algebra/Finite_dim/Finite_dim_AS_aff_gen.v
+++ b/Algebra/Finite_dim/Finite_dim_AS_aff_gen.v
@@ -100,49 +100,49 @@ Lemma aff_gen_cas :
 Proof. move=>> ->; apply aff_span_cas. Qed.

 Lemma aff_gen_lin_gen :
-  forall {PE n} {A : 'E^n.+1} O i0,
-    aff_span A O -> lin_gen (vectP PE O) (frameF A i0) -> aff_gen PE A.
+  forall {PE n} i0 O {A : 'E^n.+1},
+    aff_span A O -> lin_gen (vectP PE O) (frameF i0 A) -> aff_gen PE A.
 Proof.
-intros PE n A O i0 HO HA; apply (vectP_inj O).
+intros PE n i0 O A HO HA; apply (vectP_inj O).
 rewrite (aff_span_lin_span i0 HO) vectP_translP; easy.
 Qed.

 Lemma aff_gen_lin_gen_rev :
-  forall {PE n} {A : 'E^n.+1} {O} i0,
-    PE O -> aff_gen PE A -> lin_gen (vectP PE O) (frameF A i0).
+  forall {PE n} i0 {O} {A : 'E^n.+1},
+    PE O -> aff_gen PE A -> lin_gen (vectP PE O) (frameF i0 A).
 Proof.
-intros PE n A O i0 HO ->; rewrite (aff_span_lin_span i0 HO) vectP_translP//.
+intros PE n i0 O A HO ->; rewrite (aff_span_lin_span i0 HO) vectP_translP//.
 Qed.

 Lemma aff_gen_lin_gen_equiv :
-  forall {PE n} {A : 'E^n.+1} {O} i0, PE O -> aff_span A O ->
-    aff_gen PE A <-> lin_gen (vectP PE O) (frameF A i0).
+  forall {PE n} i0 {O} {A : 'E^n.+1}, PE O -> aff_span A O ->
+    aff_gen PE A <-> lin_gen (vectP PE O) (frameF i0 A).
 Proof.
 intros; split; [apply aff_gen_lin_gen_rev | apply aff_gen_lin_gen]; easy.
 Qed.

 Lemma lin_gen_aff_gen :
-  forall {PV n} {u : 'V^n} (O : E) i0,
+  forall {PV n} i0 (O : E) {u : 'V^n},
    zero_closed PV ->
-    aff_gen (translP PV O) (inv_frameF O u i0) -> lin_gen PV u.
+    aff_gen (translP PV O) (inv_frameF i0 O u) -> lin_gen PV u.
 Proof.
-move=> PV n u O i0
+move=> PV n i0 O u
    /(translP_zero_closed_equiv O) HO /(aff_gen_lin_gen_rev i0 HO).
 rewrite vectP_translP frameF_inv_frameF; easy.
 Qed.

 Lemma lin_gen_aff_gen_rev :
-  forall {PV n} {u : 'V^n} (O : E) i0,
-    lin_gen PV u -> aff_gen (translP PV O) (inv_frameF O u i0).
+  forall {PV n} i0 (O : E) {u : 'V^n},
+    lin_gen PV u -> aff_gen (translP PV O) (inv_frameF i0 O u).
 Proof.
-intros PV n u O i0 Hu.
-apply (aff_gen_lin_gen O i0); try rewrite vectP_translP frameF_inv_frameF//.
+intros PV n i0 O u Hu.
+apply (aff_gen_lin_gen i0 O); try rewrite vectP_translP frameF_inv_frameF//.
 apply aff_span_inv_frameF_orig.
 Qed.

 Lemma lin_gen_aff_gen_equiv :
-  forall {PV n} {u : 'V^n} (O : E) i0, zero_closed PV ->
-    lin_gen PV u <-> aff_gen (translP PV O) (inv_frameF O u i0).
+  forall {PV n} i0 (O : E) {u : 'V^n}, zero_closed PV ->
+    lin_gen PV u <-> aff_gen (translP PV O) (inv_frameF i0 O u).
 Proof.
 intros; split; [apply lin_gen_aff_gen_rev | apply lin_gen_aff_gen; easy].
 Qed.
@@ -183,18 +183,18 @@ Section ModuleSpace_AffineSpace_R_Facts.
 Context {E : ModuleSpace R_Ring}.

 Lemma aff_gen_lin_gen_ms_equiv :
-  forall {PE : E -> Prop} {n} {A : 'E^n.+1} O i0, PE O -> aff_span_ms A O ->
+  forall {PE : E -> Prop} {n} i0 O {A : 'E^n.+1}, PE O -> aff_span_ms A O ->
    aff_gen_ms PE A <->
    lin_gen (fun u => PE (O + u)) (skipF i0 A - constF n (A i0)).
 Proof.
-intros PE n A O i0; rewrite -vectP_ms_eq -frameF_ms_eq;
+intros PE n i0 O A; rewrite -vectP_ms_eq -frameF_ms_eq;
    apply (aff_gen_lin_gen_equiv i0).
 Qed.

 Lemma lin_gen_aff_gen_ms_equiv :
-  forall {PE : E -> Prop} {n} {u : 'E^n} (O : E) i0, zero_closed PE ->
+  forall {PE : E -> Prop} {n} i0 (O : E) {u : 'E^n}, zero_closed PE ->
    lin_gen PE u <->
-    aff_gen_ms (fun A => PE (A - O)) (constF n.+1 O + insertF i0 0 u).
+    aff_gen_ms (fun A => PE (A - O)) (constF n.+1 O + insert0F i0 u).
 Proof.
 move=>>; rewrite -translP_ms_eq -inv_frameF_ms_eq; apply lin_gen_aff_gen_equiv.
 Qed.

--- a/Algebra/Finite_dim/Finite_dim_AS_aff_indep.v
+++ b/Algebra/Finite_dim/Finite_dim_AS_aff_indep.v
@@ -58,10 +58,10 @@ Context {V : ModuleSpace K}.
 Context {E : AffineSpace V}.

 Lemma aff_indep_any :
-  forall {n} {A : 'E^n.+1} i0 i,
-    lin_indep (frameF A i0) -> lin_indep (frameF A i).
+  forall {n} i0 i {A : 'E^n.+1},
+    lin_indep (frameF i0 A) -> lin_indep (frameF i A).
 Proof.
-intros n A i0 i HA; destruct (ord_eq_dec i i0) as [Hi | Hi]; try now rewrite Hi.
+intros n i0 i A HA; destruct (ord_eq_dec i i0) as [Hi | Hi]; try now rewrite Hi.
 destruct n as [| n]; [contradict Hi; rewrite !ord_one; easy |].
 intros L; unfold frameF; rewrite (vectF_change_orig (A i0))
    lc_plus_r lc_constF_r scal_opp -vect_sym vectF_skipF.
@@ -77,60 +77,60 @@ rewrite zeroF skipF_correct insertF_correct_l; easy.
 Qed.

 Lemma aff_indep_all :
-  forall {n} {A : 'E^n.+1} i, aff_indep A -> lin_indep (frameF A i).
+  forall {n} i {A : 'E^n.+1}, aff_indep A -> lin_indep (frameF i A).
 Proof. move=>>; apply aff_indep_any. Qed.

 Lemma aff_indep_all_equiv :
-  forall {n} {A : 'E^n.+1}, aff_indep A <-> forall i, lin_indep (frameF A i).
+  forall {n} {A : 'E^n.+1}, aff_indep A <-> forall i, lin_indep (frameF i A).
 Proof.
 intros; split; [intros; apply aff_indep_all; easy | intros H; apply H].
 Qed.

 Lemma aff_indep_lin_indep :
-  forall {n} {A : 'E^n.+1} i0, lin_indep (frameF A i0) -> aff_indep A.
-Proof. move=> n A i0 /(aff_indep_any i0 ord0); easy. Qed.
+  forall {n} i0 {A : 'E^n.+1}, lin_indep (frameF i0 A) -> aff_indep A.
+Proof. move=> n i0 A /(aff_indep_any i0 ord0); easy. Qed.

 Lemma aff_indep_lin_indep_rev :
-  forall {n} {A : 'E^n.+1} i0, aff_indep A -> lin_indep (frameF A i0).
+  forall {n} i0 {A : 'E^n.+1}, aff_indep A -> lin_indep (frameF i0 A).
 Proof. move=>>; apply aff_indep_any. Qed.

 Lemma aff_indep_lin_indep_equiv :
-  forall {n} {A : 'E^n.+1} i0, aff_indep A <-> lin_indep (frameF A i0).
+  forall {n} i0 {A : 'E^n.+1}, aff_indep A <-> lin_indep (frameF i0 A).
 Proof.
 intros; split; [apply aff_indep_lin_indep_rev | apply aff_indep_lin_indep].
 Qed.

 Lemma lin_indep_aff_indep_equiv :
-  forall {n} {u : 'V^n} (O : E) i0,
-    lin_indep u <-> aff_indep (inv_frameF O u i0).
+  forall {n} i0 (O : E) {u : 'V^n},
+    lin_indep u <-> aff_indep (inv_frameF i0 O u).
 Proof.
-intros n u O i0. rewrite (aff_indep_lin_indep_equiv i0) frameF_inv_frameF//.
+intros n i0 O u; rewrite (aff_indep_lin_indep_equiv i0) frameF_inv_frameF//.
 Qed.

 Lemma lin_indep_aff_indep :
-  forall {n} {u : 'V^n} (O : E) i0,
-    aff_indep (inv_frameF O u i0) -> lin_indep u.
+  forall {n} i0 (O : E) {u : 'V^n},
+    aff_indep (inv_frameF i0 O u) -> lin_indep u.
 Proof. move=>>; apply lin_indep_aff_indep_equiv. Qed.

 Lemma lin_indep_aff_indep_rev :
-  forall {n} {u : 'V^n} (O : E) i0,
-    lin_indep u -> aff_indep (inv_frameF O u i0).
+  forall {n} i0 (O : E) {u : 'V^n},
+    lin_indep u -> aff_indep (inv_frameF i0 O u).
 Proof. move=>>; apply lin_indep_aff_indep_equiv. Qed.

 Lemma aff_dep_any :
-  forall {n} {A : 'E^n.+1} i0,
-    (exists i, lin_dep (frameF A i)) -> lin_dep (frameF A i0).
+  forall {n} i0 {A : 'E^n.+1},
+    (exists i, lin_dep (frameF i A)) -> lin_dep (frameF i0 A).
 Proof.
-intros n A i0; rewrite contra_not_r_equiv not_ex_not_all_equiv.
+intros n i0 A; rewrite contra_not_r_equiv not_ex_not_all_equiv.
 intros; apply (aff_indep_any i0); easy.
 Qed.

 Lemma aff_dep_ex :
-  forall {n} {A : 'E^n.+1}, (exists i, lin_dep (frameF A i)) -> aff_dep A.
+  forall {n} {A : 'E^n.+1}, (exists i, lin_dep (frameF i A)) -> aff_dep A.
 Proof. move=>>; apply aff_dep_any. Qed.

 Lemma aff_dep_ex_equiv :
-  forall {n} {A : 'E^n.+1}, aff_dep A <-> exists i, lin_dep (frameF A i).
+  forall {n} {A : 'E^n.+1}, aff_dep A <-> exists i, lin_dep (frameF i A).
 Proof. intros; split; [intros H; exists ord0; easy | apply aff_dep_any]. Qed.

 Lemma aff_indep_decomp_uniq :
@@ -149,7 +149,7 @@ Lemma aff_indep_decomp_uniq_rev :
 Proof.
 intros n A HA L HL; apply (insertF_inj_r ord0 (1 - sum L) 1).
 replace (insertF _ _ L) with (part1F0 L) by easy; rewrite -itemF_insertF.
-assert (H1 : sum (part1F L ord0) = 1) by apply part1F_sum.
+assert (H1 : sum (part1F ord0 L) = 1) by apply part1F_sum.
 assert (H2 : sum (itemF n.+1 ord0 1) = (1 : K)) by now apply sum_itemF.
 apply HA; [easy.. |]; apply (vect_l_inj (A ord0)).
 rewrite -(scal_one_l 1 (_ --> barycenter (part1F _ _) _))// -{1}H1
@@ -213,7 +213,7 @@ Lemma aff_indep_monot :
    injective A1 -> invalF A1 A2 -> aff_indep A2 -> aff_indep A1.
 Proof.
 intros n1 n2 A1 A2 HA1 HA HA2; destruct (HA ord0) as [i2 Hi2].
-apply (lin_indep_monot (frameF A2 i2)).
+apply (lin_indep_monot (frameF i2 A2)).
 apply frameF_inj_equiv, skipF_inj; easy.
 apply frameF_invalF_equiv; [| apply skipF_invalF]; easy.
 apply aff_indep_all; easy.
@@ -244,9 +244,9 @@ Lemma aff_indep_coupleF_equiv :
 Proof. intros; rewrite aff_indep_2_equiv coupleF_0 coupleF_1; easy. Qed.

 Lemma aff_indep_skipF :
-  forall {n} {A : 'E^n.+2} i0, aff_indep A -> aff_indep (skipF i0 A).
+  forall {n} i0 {A : 'E^n.+2}, aff_indep A -> aff_indep (skipF i0 A).
 Proof.
-intros n A i0 HA; destruct (ord_eq_dec i0 ord0) as [Hi0 | Hi0]; [subst |].
+intros n i0 A HA; destruct (ord_eq_dec i0 ord0) as [Hi0 | Hi0]; [subst |].
 (* *)
 apply (aff_indep_any ord_max); rewrite -(insert_ord_max ord_max_not_0).
 rewrite frameF_skipF_alt; apply lin_indep_skipF_compat, aff_indep_all; easy.
@@ -256,25 +256,25 @@ rewrite frameF_skipF; apply lin_indep_skipF_compat; easy.
 Qed.

 Lemma aff_indep_permutF :
-  forall {n} {A : 'E^n.+1} {p},
+  forall {n p} {A : 'E^n.+1},
    bijective p -> aff_indep A -> aff_indep (permutF p A).
 Proof.
-intros n A p Hp HA; apply (aff_indep_any (p ord0)).
+intros n p A Hp HA; apply (aff_indep_any (p ord0)).
 rewrite (frameF_permutF (bij_inj Hp)); apply lin_indep_permutF.
 apply skip_f_ord_bij.
 apply aff_indep_all; easy.
 Qed.

 Lemma aff_indep_permutF_rev :
-  forall {n} {A : 'E^n.+1} p,
+  forall {n p} {A : 'E^n.+1},
    bijective p -> aff_indep (permutF p A) -> aff_indep A.
 Proof.
-intros n A p Hp; rewrite {2}(permutF_f_inv_l Hp A).
+intros n p A Hp; rewrite {2}(permutF_f_inv_l Hp A).
 apply aff_indep_permutF, f_inv_bij.
 Qed.

 Lemma aff_indep_permutF_equiv :
-  forall {n} {A : 'E^n.+1} p,
+  forall {n p} {A : 'E^n.+1},
    bijective p -> aff_indep A <-> aff_indep (permutF p A).
 Proof.
 intros; split; [apply aff_indep_permutF | apply aff_indep_permutF_rev]; easy.

--- a/Algebra/Finite_dim/Finite_dim_AS_aff_map.v
+++ b/Algebra/Finite_dim/Finite_dim_AS_aff_map.v
@@ -106,7 +106,7 @@ Lemma baryc_bc_baryc :
  forall {p} L (B : 'E^p), sum L = 1 -> inclF B (aff_span A) ->
    barycenter (barycenter_ms L (mapF (baryc_coord A) B)) A = barycenter L B.
 Proof.
-intros p L B HL HB; rewrite baryc_ms_eq// -(barycenter2_r_alt _ B)//.
+intros p L B HL HB; rewrite baryc_ms_eq// -(barycenter2_r_alt _ _ B)//.
 apply invertible_eq_one; easy.
 1,2: intro; rewrite mapF_correct; apply bc_correct; easy.
 Qed.

--- a/Algebra/Finite_dim/Finite_dim_AS_aff_span.v
+++ b/Algebra/Finite_dim/Finite_dim_AS_aff_span.v
@@ -176,9 +176,9 @@ intros; apply subset_ext_equiv; split; apply aff_span_monot_inclF; easy.
 Qed.

 Lemma aff_span_inv_frameF_orig :
-  forall {n} (B : 'V^n) (O : E) i0, aff_span (inv_frameF O B i0) O.
+  forall {n} i0 (O : E) (B : 'V^n), aff_span (inv_frameF i0 O B) O.
 Proof.
-intros n B O i0; rewrite -{2}(transl_zero O); apply (aff_span_ub _ _ i0).
+intros n i0 O B; rewrite -{2}(transl_zero O); apply (aff_span_ub _ _ i0).
 unfold inv_frameF; rewrite translF_insertF insertF_correct_l; easy.
 Qed.

@@ -285,10 +285,10 @@ intros B HB; apply HB; [apply aff_span_cas | apply aff_span_inclF_diag].
 Qed.

 Lemma lin_span_aff_span_aux :
-  forall {n} {A : 'E^n.+1} {O} i0, aff_span A O ->
-    lin_span (frameF A i0) = vectP (aff_span A) O.
+  forall {n} i0 {O} {A : 'E^n.+1}, aff_span A O ->
+    lin_span (frameF i0 A) = vectP (aff_span A) O.
 Proof.
-intros n A O i0 HO; rewrite (vectP_orig_indep (A i0) HO).
+intros n i0 O A HO; rewrite (vectP_orig_indep (A i0) HO).
 2: { apply cas_cms_equiv_R; try apply aff_span_inclF_diag.
    move=>> HL HC; apply aff_span_cas; easy. }
 apply eq_sym, subset_ext_equiv; split; unfold vectP, preimage; intros u Hu.
@@ -305,8 +305,8 @@ apply Aff_span, invertible_eq_one, sum_insertF_baryc.
 Qed.

 Lemma lin_span_aff_span :
-  forall {n} {u : 'V^n} (O : E) i0,
-    lin_span u = vectP (aff_span (inv_frameF O u i0)) O.
+  forall {n} i0 (O : E) {u : 'V^n},
+    lin_span u = vectP (aff_span (inv_frameF i0 O u)) O.
 Proof.
 intros; rewrite -(lin_span_aff_span_aux i0).
 rewrite frameF_inv_frameF; easy.
@@ -314,11 +314,11 @@ apply aff_span_inv_frameF_orig.
 Qed.

 Lemma aff_span_lin_span :
-  forall {n} {A : 'E^n.+1} {O} i0, aff_span A O ->
-    aff_span A = translP (lin_span (frameF A i0)) O.
+  forall {n} i0 {O} {A : 'E^n.+1}, aff_span A O ->
+    aff_span A = translP (lin_span (frameF i0 A)) O.
 Proof.
-intros n A O i0 HO; apply (vectP_inj O).
-rewrite vectP_translP (lin_span_aff_span (A i0) i0) inv_frameF_frameF.
+intros n i0 O A HO; apply (vectP_inj O).
+rewrite vectP_translP (lin_span_aff_span i0 (A i0)) inv_frameF_frameF.
 apply vectP_orig_indep; [easy | apply cas_cms].
 apply aff_span_inclF_diag.
 apply invertible_equiv_R, two_not_zero_R.
@@ -339,14 +339,14 @@ Lemma aff_span_ext_ms :
 Proof. move=>>; apply aff_span_ext. Qed.

 Lemma lin_span_aff_span_ms :
-  forall {n} {u : 'E^n} O i0, lin_span u =
-    fun v => aff_span_ms (constF n.+1 O + insertF i0 0 u) (O + v).
+  forall {n} i0 O {u : 'E^n}, lin_span u =
+    fun v => aff_span_ms (constF n.+1 O + insert0F i0 u) (O + v).
 Proof.
 intros; rewrite -inv_frameF_ms_eq -vectP_ms_eq; apply lin_span_aff_span.
 Qed.

 Lemma aff_span_lin_span_ms :
-  forall {n} {A : 'E^n.+1} {O} i0, aff_span_ms A O ->
+  forall {n} i0 {O} {A : 'E^n.+1}, aff_span_ms A O ->
    aff_span_ms A = fun B => lin_span (skipF i0 A - constF n (A i0)) (B - O).
 Proof.
 intros; rewrite -frameF_ms_eq -translP_ms_eq; apply aff_span_lin_span; easy.

--- a/Algebra/Finite_dim/Finite_dim_AS_def.v
+++ b/Algebra/Finite_dim/Finite_dim_AS_def.v
@@ -157,7 +157,7 @@ Lemma aff_gen_ext2 :
    PE1 = PE2 -> A1 = A2 -> aff_gen PE1 A1 -> aff_gen PE2 A2.
 Proof. intros; subst; easy. Qed.

-Definition aff_indep {n} (A : 'E^n.+1) : Prop := lin_indep (frameF A ord0).
+Definition aff_indep {n} (A : 'E^n.+1) : Prop := lin_indep (frameF ord0 A).

 Lemma aff_indep_ext :
  forall {n} (A1 : 'E^n.+1) {A2}, A1 = A2 -> aff_indep A1 -> aff_indep A2.

--- a/Algebra/Finite_dim/Finite_dim_MS_lin_indep.v
+++ b/Algebra/Finite_dim/Finite_dim_MS_lin_indep.v
@@ -174,18 +174,18 @@ rewrite concatF_correct_l concat_l_first
 Qed.

 Lemma lin_dep_insertF_compat :
-  forall {n} {B : 'E^n} x0 i0, lin_dep B -> lin_dep (insertF i0 x0 B).
+  forall {n} i0 x0 {B : 'E^n}, lin_dep B -> lin_dep (insertF i0 x0 B).
 Proof.
-intros n B x0 i0; rewrite 2!lin_dep_ex; move=> [L [HL /nextF_rev [i Hi]]].
+intros n i0 x0 B; rewrite 2!lin_dep_ex; move=> [L [HL /nextF_rev [i Hi]]].
 exists (insertF i0 0 L); split.
 rewrite lc_insertF scal_zero_l HL plus_zero_l; easy.
 apply nextF; exists (skip_ord i0 i); rewrite insertF_correct; easy.
 Qed.

 Lemma lin_dep_skipF_reg :
-  forall {n} {B : 'E^n.+1} i0, lin_dep (skipF i0 B) -> lin_dep B.
+  forall {n} i0 {B : 'E^n.+1}, lin_dep (skipF i0 B) -> lin_dep B.
 Proof.
-intros n B i0; rewrite -{2}(insertF_skipF i0 B).
+intros n i0 B; rewrite -{2}(insertF_skipF i0 B).
 apply lin_dep_insertF_compat.
 Qed.

@@ -308,11 +308,11 @@ intros [H1 H2]; eapply lin_dep_concatF_not_disjF; [apply H1 | easy].
 Qed.

 Lemma lin_indep_insertF_reg :
-  forall {n} {B : 'E^n} x0 i0, lin_indep (insertF i0 x0 B) -> lin_indep B.
+  forall {n} i0 x0 {B : 'E^n}, lin_indep (insertF i0 x0 B) -> lin_indep B.
 Proof. move=>>; rewrite contra_equiv; apply lin_dep_insertF_compat. Qed.

 Lemma lin_indep_skipF_compat :
-  forall {n} {B : 'E^n.+1} i0, lin_indep B -> lin_indep (skipF i0 B).
+  forall {n} i0 {B : 'E^n.+1}, lin_indep B -> lin_indep (skipF i0 B).
 Proof. move=>>; rewrite contra_equiv; apply lin_dep_skipF_reg. Qed.

 Lemma lin_indep_not_line :
@@ -423,16 +423,16 @@ Qed.
 #<A HREF="##GostiauxT1">#[[GostiauxT1]]#</A>#
 Th 6.61, pp. 189-190. (=>) *)
 Lemma lin_dep_insertF :
-  forall {n} {B : 'E^n} {x0} i0, lin_span B x0 -> lin_dep (insertF i0 x0 B).
+  forall {n} i0 {x0} {B : 'E^n}, lin_span B x0 -> lin_dep (insertF i0 x0 B).
 Proof.
-intros n B x0 i0 [L]; apply lin_dep_ex; exists (insertF i0 (- 1%K) L); split.
+intros n i0 x0 B [L]; apply lin_dep_ex; exists (insertF i0 (- 1%K) L); split.
 rewrite lc_insertF scal_opp_l scal_one; apply: plus_opp_l.
 rewrite -(insertF_zero i0); apply insertF_nextF_compat_l.
 apply one_not_zero in HK; contradict HK; apply opp_inj; rewrite opp_zero; easy.
 Qed.

 Lemma lin_indep_insertF_rev :
-  forall {n} {B : 'E^n} {x0} i0,
+  forall {n} i0 {x0} {B : 'E^n},
    lin_indep (insertF i0 x0 B) -> ~ lin_span B x0.
 Proof. move=>>; rewrite contra_not_r_equiv; apply lin_dep_insertF. Qed.


--- a/Algebra/Finite_dim/Finite_dim_MS_lin_indep_R.v
+++ b/Algebra/Finite_dim/Finite_dim_MS_lin_indep_R.v
@@ -265,10 +265,10 @@ Proof. move=>>; rewrite -contra_equiv; apply lin_indep_coupleF_sym. Qed.
 #<A HREF="##GostiauxT1">#[[GostiauxT1]]#</A>#
 Th 6.61, pp. 189-190. (<=) *)
 Lemma lin_dep_insertF_rev :
-  forall {n} {B : 'E^n} {x0} i0,
+  forall {n} i0 {x0} {B : 'E^n},
    lin_indep B -> lin_dep (insertF i0 x0 B) -> lin_span B x0.
 Proof.
-move=> n B x0 i0 HB /lin_dep_ex [L [HL1 HL2]];
+move=> n i0 x0 B HB /lin_dep_ex [L [HL1 HL2]];
    rewrite lc_insertF_r in HL1.
 destruct (Hierarchy.eq_dec (L i0) 0) as [HL3 | HL3].
 (* *)
@@ -288,7 +288,7 @@ Qed.
 #<A HREF="##GostiauxT1">#[[GostiauxT1]]#</A>#
 Th 6.61, pp. 189-190. (<=>) *)
 Lemma lin_dep_insertF_equiv :
-  forall {n} {B : 'E^n} {x0} i0,
+  forall {n} i0 {x0} {B : 'E^n},
    lin_indep B -> lin_dep (insertF i0 x0 B) <-> lin_span B x0.
 Proof.
 intros; split; [apply lin_dep_insertF_rev; easy |
@@ -296,14 +296,14 @@ intros; split; [apply lin_dep_insertF_rev; easy |
 Qed.

 Lemma lin_indep_insertF :
-  forall {n} {B : 'E^n} {x0} i0,
+  forall {n} i0 {x0} {B : 'E^n},
    lin_indep B -> ~ lin_span B x0 -> lin_indep (insertF i0 x0 B).
 Proof.
 move=>> HB; rewrite contra_not_l_equiv; apply lin_dep_insertF_rev; easy.
 Qed.

 Lemma lin_indep_insertF_equiv :
-  forall {n} {B : 'E^n} {x0} i0,
+  forall {n} i0 {x0} {B : 'E^n},
    lin_indep B -> lin_indep (insertF i0 x0 B) <-> ~ lin_span B x0.
 Proof. move=>>; rewrite iff_not_r_equiv; apply lin_dep_insertF_equiv. Qed.


--- a/Algebra/Group/Group_compl.v
+++ b/Algebra/Group/Group_compl.v
@@ -304,36 +304,36 @@ Lemma concatF_minus :
 Proof. intros; rewrite !minus_eq concatF_plus concatF_opp; easy. Qed.

 Lemma insertF_opp :
-  forall {n} (A : 'G^n) a0 i0, insertF i0 (-a0) (- A) = - insertF i0 a0 A.
+  forall {n} i0 a0 (A : 'G^n), insertF i0 (-a0) (- A) = - insertF i0 a0 A.
 Proof.
-intros n A a i0; extF i; rewrite fct_opp_eq;
+intros n i0 a A; extF i; rewrite fct_opp_eq;
    destruct (ord_eq_dec i i0) as [Hi | Hi];
    [rewrite !insertF_correct_l | rewrite !insertF_correct_r]; easy.
 Qed.

 Lemma insertF_minus :
-  forall {n} (A B : 'G^n) a0 b0 i0,
+  forall {n} i0 a0 b0 (A B : 'G^n),
    insertF i0 (a0 - b0) (A - B) = insertF i0 a0 A - insertF i0 b0 B.
 Proof. intros; rewrite !minus_eq insertF_plus insertF_opp; easy. Qed.

-Lemma skipF_opp : forall {n} (A : 'G^n.+1) i0, skipF i0 (- A) = - skipF i0 A.
+Lemma skipF_opp : forall {n} i0 (A : 'G^n.+1), skipF i0 (- A) = - skipF i0 A.
 Proof. easy. Qed.

 Lemma skipF_minus :
-  forall {n} (A B : 'G^n.+1) i0, skipF i0 (A - B) = skipF i0 A - skipF i0 B.
+  forall {n} i0 (A B : 'G^n.+1), skipF i0 (A - B) = skipF i0 A - skipF i0 B.
 Proof. easy. Qed.

 Lemma replaceF_opp :
-  forall {n} (A : 'G^n.+1) a0 i0,
+  forall {n} i0 a0 (A : 'G^n.+1),
    replaceF i0 (- a0) (- A) = - replaceF i0 a0 A.
 Proof.
-intros n A a0 i0; extF i; rewrite fct_opp_eq;
+intros n i0 a0 A; extF i; rewrite fct_opp_eq;
    destruct (ord_eq_dec i i0) as [Hi | Hi];
    [rewrite !replaceF_correct_l | rewrite !replaceF_correct_r]; easy.
 Qed.

 Lemma replaceF_minus :
-  forall {n} (A B : 'G^n.+1) a0 b0 i0,
+  forall {n} i0 a0 b0 (A B : 'G^n.+1),
    replaceF i0 (a0 - b0) (A - B) = replaceF i0 a0 A - replaceF i0 b0 B.
 Proof. intros; rewrite !minus_eq replaceF_plus replaceF_opp; easy. Qed.

@@ -350,9 +350,9 @@ Proof. easy. Qed.
 (** [mapF_minus] is [f_minus_compat_mapF] in [Group_morphism]. *)

 Lemma sum_squeezeF :
-  forall {n} (u : 'G^n.+1) {i0 i1}, i1 <> i0 -> sum (squeezeF i0 i1 u) = sum u.
+  forall {n} {i0 i1} (H : i1 <> i0) (u : 'G^n.+1), sum (squeezeF i0 i1 u) = sum u.
 Proof.
-intros n u i0 i1 Hi.
+intros n i0 i1 Hi u.
 apply (plus_reg_l (u i0 + replaceF i0 (u i0 + u i1) u i1)).
 rewrite -plus_assoc -sum_skipF replaceF_correct_r//.
 rewrite sum_replaceF; easy.

--- a/Algebra/ModuleSpace/ModuleSpace_FF_FT.v
+++ b/Algebra/ModuleSpace/ModuleSpace_FF_FT.v
@@ -267,7 +267,7 @@ Lemma scalF_liftF_S :
 Proof. easy. Qed.

 Lemma scalF_insertF :
-  forall {n} a a0 (u : 'E^n) x0 i0,
+  forall {n} i0 a0 x0 a (u : 'E^n),
    scalF (insertF i0 a0 a) (insertF i0 x0 u) =
      insertF i0 (scal a0 x0) (scalF a u).
 Proof.
@@ -276,23 +276,23 @@ intros; extF; rewrite scalF_correct; unfold insertF;
 Qed.

 Lemma scalF_insert2F :
-  forall {n} a a0 a1 (u : 'E^n) x0 x1 {i0 i1} (H : i1 <> i0),
+  forall {n} {i0 i1} (H : i1 <> i0) a0 a1 x0 x1 a (u : 'E^n),
    scalF (insert2F H a0 a1 a) (insert2F H x0 x1 u) =
      insert2F H (scal a0 x0) (scal a1 x1) (scalF a u).
 Proof. intros; rewrite 3!insert2F_correct 2!scalF_insertF; easy. Qed.

 Lemma scalF_skipF :
-  forall {n} a (u : 'E^n.+1) i0,
+  forall {n} i0 a (u : 'E^n.+1),
    scalF (skipF i0 a) (skipF i0 u) = skipF i0 (scalF a u).
 Proof. easy. Qed.

 Lemma scalF_skip2F :
-  forall {n} a (u : 'E^n.+2) {i0 i1} (H : i1 <> i0),
+  forall {n} {i0 i1} (H : i1 <> i0) a (u : 'E^n.+2),
    scalF (skip2F H a) (skip2F H u) = skip2F H (scalF a u).
 Proof. easy. Qed.

 Lemma scalF_replaceF :
-  forall {n} a a0 (u : 'E^n) x0 i0,
+  forall {n} i0 a0 x0 a (u : 'E^n),
    scalF (replaceF i0 a0 a) (replaceF i0 x0 u) =
      replaceF i0 (scal a0 x0) (scalF a u).
 Proof.
@@ -300,7 +300,7 @@ intros; rewrite 3!replaceF_equiv_def_skipF scalF_skipF scalF_insertF; easy.
 Qed.

 Lemma scalF_replace2F :
-  forall {n} a a0 a1 (u : 'E^n) x0 x1 i0 i1,
+  forall {n} i0 i1 a0 a1 x0 x1 a (u : 'E^n),
    scalF (replace2F i0 i1 a0 a1 a) (replace2F i0 i1 x0 x1 u) =
      replace2F i0 i1 (scal a0 x0) (scal a1 x1) (scalF a u).
 Proof. intros; rewrite 2!scalF_replaceF; easy. Qed.
@@ -459,27 +459,27 @@ intros n1 n2 l A1 A2; extF i; rewrite !fct_scal_eq;
 Qed.

 Lemma insertF_scal :
-  forall {n} l (A : 'E^n) a0 i0,
+  forall {n} i0 l a0 (A : 'E^n),
    insertF i0 (scal l a0) (scal l A) = scal l insertF i0 a0 A.
 Proof.
-intros n l A a0 i0; extF i; rewrite !fct_scal_eq;
+intros n i0 l a0 A; extF i; rewrite !fct_scal_eq;
    destruct (ord_eq_dec i i0);
    [rewrite !insertF_correct_l | rewrite !insertF_correct_r]; easy.
 Qed.

 Lemma insert0F_scal :
-  forall {n} l (A : 'E^n) i0, insert0F i0 (scal l A) = scal l insert0F i0 A.
+  forall {n} i0 l (A : 'E^n), insert0F i0 (scal l A) = scal l insert0F i0 A.
 Proof. intros; rewrite -{1}(scal_zero_r l) insertF_scal; easy. Qed.

 Lemma skipF_scal :
-  forall {n} l (A : 'E^n.+1) i0, skipF i0 (scal l A) = scal l skipF i0 A.
+  forall {n} i0 l (A : 'E^n.+1), skipF i0 (scal l A) = scal l skipF i0 A.
 Proof. easy. Qed.

 Lemma replaceF_scal :
-  forall {n} l (A : 'E^n.+1) a0 i0,
+  forall {n} i0 l a0 (A : 'E^n.+1),
    replaceF i0 (scal l a0) (scal l A) = scal l replaceF i0 a0 A.
 Proof.
-intros n l A a0 i0; extF i; rewrite !fct_scal_eq;
+intros n i0 l a0 A; extF i; rewrite !fct_scal_eq;
    destruct (ord_eq_dec i i0);
    [rewrite !replaceF_correct_l | rewrite !replaceF_correct_r]; easy.
 Qed.

--- a/Algebra/ModuleSpace/ModuleSpace_R_compl.v
+++ b/Algebra/ModuleSpace/ModuleSpace_R_compl.v
@@ -533,7 +533,7 @@ Qed.
 Lemma dot_product_def : forall {n} (u : 'R^n), u ⋅ u = 0 -> u = 0.
 Proof.
 intros n u; induction n as [| n Hn]; [intros; apply hat0F_eq; easy |].
-rewrite (dot_product_skipF _ _ ord0); intros Hu.
+rewrite (dot_product_skipF ord0); intros Hu.
 apply Rplus_eq_R0 in Hu; try apply scal_pos_R; try apply dot_product_pos.
 destruct Hu as [Hu0 Hu].
 apply (extF_zero_skipF ord0); [apply scal_def_R | apply Hn]; easy.
@@ -618,7 +618,7 @@ Section Lin_map_Euclidean_space_R_Facts.

 Lemma part1F_fct_lm :
  forall {n} (i0 : 'I_n.+1),
-    lin_map (part1F^~ i0 - (fun=> part1F 0 i0) : 'R^n -> 'R^n.+1).
+    lin_map (part1F i0 - (fun=> part1F i0 0) : 'R^n -> 'R^n.+1).
 Proof.
 intros n i0; apply lm_scatter_rev; intros i; split.
 (* *)

--- a/Algebra/ModuleSpace/ModuleSpace_compl.v
+++ b/Algebra/ModuleSpace/ModuleSpace_compl.v
@@ -203,6 +203,9 @@ Proof. intros; subst; apply scal_one. Qed.
 Lemma scal_one_r : forall (a b : K), b = 1 -> scal a b = a.
 Proof. intros; subst; apply mult_one_r. Qed.

+Lemma scal_ones : forall {n} a (b : 'K^n), b = 1 -> scal a b = constF n a.
+Proof. intros; subst; extF; apply scal_one_r; easy. Qed.
+
 Lemma scal_sum_l :
  forall {n} (a : 'K^n) (u : E), scal (sum a) u = sum (fun i => scal (a i) u).
 Proof.

--- a/Algebra/ModuleSpace/ModuleSpace_lin_comb.v
+++ b/Algebra/ModuleSpace/ModuleSpace_lin_comb.v
@@ -326,7 +326,7 @@ Proof. intros; rewrite lc_splitF firstF_concatF lastF_concatF; easy. Qed.
 Lemma lc_skipF :
  forall {n} {L} {B : 'E^n.+1} i0,
    lin_comb L B =  scal (L i0) (B i0) + lin_comb (skipF i0 L) (skipF i0 B).
-Proof. intros n L B i0; unfold lin_comb; rewrite (sum_skipF _ i0); easy. Qed.
+Proof. intros n L B i0; unfold lin_comb; rewrite (sum_skipF i0); easy. Qed.

 Lemma lc_skipF_ex_l :
  forall {n} L0 L1 (B : 'E^n.+1) i0,
@@ -423,76 +423,75 @@ assert (HL1b : skipFmax L1 = L) by apply skipF_insertF.
 rewrite -skipF_last -{1}HL1b -lc_skip_zero_l// -insertF_concatF_max; easy.
 Qed.

+Lemma lc_insertF :
+  forall {n} i0 a0 x0 L (B : 'E^n),
+    lin_comb (insertF i0 a0 L) (insertF i0 x0 B) = scal a0 x0 + lin_comb L B.
+Proof. intros; unfold lin_comb; rewrite scalF_insertF; apply sum_insertF. Qed.
+
+Lemma lc_insertF_l :
+  forall {n} i0 a0 L (B : 'E^n.+1),
+    lin_comb (insertF i0 a0 L) B = scal a0 (B i0) + lin_comb L (skipF i0 B).
+Proof.
+intros n i0 a0 L B; rewrite -{1}(insertF_skipF i0 B) lc_insertF; easy.
+Qed.
+
+Lemma lc_insertF_r :
+  forall {n} i0 x0 L (B : 'E^n),
+    lin_comb L (insertF i0 x0 B) = scal (L i0) x0 + lin_comb (skipF i0 L) B.
+Proof.
+intros n i0 x0 L B; rewrite -{1}(insertF_skipF i0 L) lc_insertF; easy.
+Qed.
+
+Lemma lc_insert2F :
+  forall {n} {i0 i1} (H : i1 <> i0) x0 x1 a0 a1 L (B : 'E^n),
+    lin_comb (insert2F H a0 a1 L) (insert2F H x0 x1 B) =
+      scal a0 x0 + scal a1 x1 + lin_comb L B.
+Proof. intros; unfold lin_comb; rewrite scalF_insert2F; apply sum_insert2F. Qed.
+
 Lemma lc_skip2F :
-  forall {n} L (B : 'E^n.+2) {i0 i1} (H : i1 <> i0),
+  forall {n i0 i1} (H : i1 <> i0) L (B : 'E^n.+2),
    lin_comb L B =
      scal (L i0) (B i0) + scal (L i1) (B i1) +
      lin_comb (skip2F H L) (skip2F H B).
 Proof.
-intros n L B i0 i1 H; unfold lin_comb; rewrite (sum_skip2F _ H); easy.
+intros n i0 i1 H L B; unfold lin_comb; rewrite (sum_skip2F H); easy.
 Qed.

 Lemma lc_two :
-  forall {n L} {B : 'E^n.+2} {i0 i1 : 'I_n.+2} (H : (i1 <> i0)%nat),
+  forall {n} {i0 i1 : 'I_n.+2} (H : (i1 <> i0)%nat) {L} {B : 'E^n.+2},
    skip2F H (scalF L B) = 0 ->
    lin_comb L B = scal (L i0) (B i0) + scal (L i1) (B i1).
 Proof. move=>>; rewrite -!scalF_correct; apply sum_two. Qed.

 Lemma lc_two_l :
-  forall {n L} {B : 'E^n.+2} {i0 i1} (H : i1 <> i0),
+  forall {n i0 i1} (H : i1 <> i0) {L} {B : 'E^n.+2},
    skip2F H L = 0 ->
    lin_comb L B = scal (L i0) (B i0) + scal (L i1) (B i1).
 Proof.
-intros n L B i0 i1 Hi H; apply lc_two with Hi; rewrite -scalF_skip2F.
+intros n i0 i1 Hi L B H; apply lc_two with Hi; rewrite -scalF_skip2F.
 apply scalF_zero_compat_l; easy.
 Qed.

 Lemma lc_two_r :
-  forall {n L} {B : 'E^n.+2} {i0 i1} (H : i1 <> i0),
+  forall {n i0 i1} (H : i1 <> i0) {L} {B : 'E^n.+2},
    skip2F H B = 0 ->
    lin_comb L B = scal (L i0) (B i0) + scal (L i1) (B i1).
 Proof.
-intros n L B i0 i1 Hi H; apply lc_two with Hi; rewrite -scalF_skip2F.
+intros n i0 i1 Hi L B H; apply lc_two with Hi; rewrite -scalF_skip2F.
 apply scalF_zero_compat_r; easy.
 Qed.

-Lemma lc_insertF :
-  forall {n} L (B : 'E^n) a0 x0 i0,
-    lin_comb (insertF i0 a0 L) (insertF i0 x0 B) = scal a0 x0 + lin_comb L B.
-Proof. intros; unfold lin_comb; rewrite scalF_insertF; apply sum_insertF. Qed.
-
-Lemma lc_insertF_l :
-  forall {n} L (B : 'E^n.+1) a0 i0,
-    lin_comb (insertF i0 a0 L) B = scal a0 (B i0) + lin_comb L (skipF i0 B).
-Proof.
-intros n L B a0 i0; rewrite -{1}(insertF_skipF i0 B) lc_insertF; easy.
-Qed.
-
-Lemma lc_insertF_r :
-  forall {n} L (B : 'E^n) x0 i0,
-    lin_comb L (insertF i0 x0 B) = scal (L i0) x0 + lin_comb (skipF i0 L) B.
-Proof.
-intros n L B x0 i0; rewrite -{1}(insertF_skipF i0 L) lc_insertF; easy.
-Qed.
-
-Lemma lc_insert2F :
-  forall {n} L (B : 'E^n) a0 a1 x0 x1 {i0 i1} (H : i1 <> i0),
-    lin_comb (insert2F H a0 a1 L) (insert2F H x0 x1 B) =
-      scal a0 x0 + scal a1 x1 + lin_comb L B.
-Proof. intros; unfold lin_comb; rewrite scalF_insert2F; apply sum_insert2F. Qed.
-
 Lemma lc_replaceF :
-  forall {n} L (B : 'E^n) a0 x0 i0,
+  forall {n} i0 a0 x0 L (B : 'E^n),
    scal (L i0) (B i0) + lin_comb (replaceF i0 a0 L) (replaceF i0 x0 B) =
      scal a0 x0 + lin_comb L B.
 Proof.
-intros [| n] L B a0 x0 i0; [destruct i0; easy |].
+intros [| n] i0 a0 x0 L B; [destruct i0; easy |].
 unfold lin_comb; rewrite scalF_replaceF -scalF_correct; apply sum_replaceF.
 Qed.

 Lemma lc_replace2F :
-  forall {n} L (B : 'E^n.+2) a0 a1 x0 x1 {i0 i1},
-    i1 <> i0 ->
+  forall {n} {i0 i1} (H : i1 <> i0) a0 a1 x0 x1 L (B : 'E^n.+2),
    scal (L i0) (B i0) + scal (L i1) (B i1) +
        lin_comb (replace2F i0 i1 a0 a1 L) (replace2F i0 i1 x0 x1 B) =
      scal a0 x0 + scal a1 x1 + lin_comb L B.
@@ -502,8 +501,7 @@ intros; unfold lin_comb; rewrite scalF_replace2F -!scalF_correct;
 Qed.

 Lemma lc_replace2F_eq :
-  forall {n} L (B : 'E^n.+2) a0 a1 x0 x1 {i0 i1},
-    i1 = i0 ->
+  forall {n} {i0 i1} (H : i1 = i0) a0 a1 x0 x1 L (B : 'E^n.+2),
    scal (L i1) (B i1) +
        lin_comb (replace2F i0 i1 a0 a1 L) (replace2F i0 i1 x0 x1 B) =
      scal a1 x1 + lin_comb L B.
@@ -1005,12 +1003,12 @@ Lemma dot_product_ind_l :
 Proof. intros; unfold dot_product; rewrite lc_ind_l; easy. Qed.

 Lemma dot_product_insertF :
-  forall {n} (u v : 'K^n) a b i0,
+  forall {n} i0 a b (u v : 'K^n),
    insertF i0 a u ⋅ insertF i0 b v = a * b + u ⋅ v.
 Proof. intros; unfold dot_product; rewrite lc_insertF; easy. Qed.

 Lemma dot_product_skipF :
-  forall {n} (u v : 'K^n.+1) i0,
+  forall {n} i0 (u v : 'K^n.+1),
    u ⋅ v = scal (u i0) (v i0) + skipF i0 u ⋅ skipF i0 v.
 Proof. intros; unfold dot_product; apply lc_skipF. Qed.


--- a/Algebra/Monoid/MonoidMult.v
+++ b/Algebra/Monoid/MonoidMult.v
@@ -110,7 +110,7 @@ Lemma sum_absorbing :
  forall x0 {n} (u : 'G^n), absorbing x0 -> inF x0 u -> sum u = x0.
 Proof.
 intros x0 [| n] u Hx0 [i0 Hu]; [now destruct i0 |].
-rewrite (sum_skipF _ i0) -Hu; easy.
+rewrite (sum_skipF i0) -Hu; easy.
 Qed.

 End Multiplicative_Monoid_Facts.
@@ -172,7 +172,7 @@ Lemma prod_nat_one_compat : forall {n} (u : 'nat_mul^n), u = 1 -> prod_nat u = 1
 Proof. move=>>; apply sum_zero_compat. Qed.

 Lemma prod_nat_singl :
-  forall {n} (u : 'nat_mul^n.+1) i0, skipF i0 u = 1 -> prod_nat u = u i0.
+  forall {n} i0 (u : 'nat_mul^n.+1), skipF i0 u = 1 -> prod_nat u = u i0.
 Proof. move=>>; apply sum_one. Qed.

 Lemma prod_nat_castF :
@@ -193,7 +193,7 @@ Lemma prod_nat_concatF :
 Proof. intros; apply sum_concatF. Qed.

 Lemma prod_nat_replaceF :
-  forall {n} (u : 'nat_mul^n.+1) x0 i0,
+  forall {n} i0 x0 (u : 'nat_mul^n.+1),
    u i0 * prod_nat (replaceF i0 x0 u) = x0 * prod_nat u.
 Proof. intros; apply sum_replaceF. Qed.

@@ -266,7 +266,7 @@ Lemma prod_R_one_compat : forall {n} (u : 'R_mul^n), u = 1 -> prod_R u = 1.
 Proof. move=>>; apply sum_zero_compat. Qed.

 Lemma prod_R_singl :
-  forall {n} (u : 'R_mul^n.+1) i0, skipF i0 u = 1 -> prod_R u = u i0.
+  forall {n} i0 (u : 'R_mul^n.+1), skipF i0 u = 1 -> prod_R u = u i0.
 Proof. move=>>; apply sum_one. Qed.

 Lemma prod_R_castF :
@@ -286,7 +286,7 @@ Lemma prod_R_concatF :
 Proof. intros; apply sum_concatF. Qed.

 Lemma prod_R_replaceF :
-  forall {n} (u : 'R_mul^n.+1) x0 i0,
+  forall {n} i0 x0 (u : 'R_mul^n.+1),
    u i0 * prod_R (replaceF i0 x0 u) = x0 * prod_R u.
 Proof. intros; apply sum_replaceF. Qed.


--- a/Algebra/Monoid/Monoid_FF.v
+++ b/Algebra/Monoid/Monoid_FF.v
@@ -524,7 +524,7 @@ Proof. move=>> HA H0; rewrite HA H0; apply insertF_zero. Qed.

 Lemma insert2F_zero_compat :
  forall {n} {i0 i1} (H : i1 <> i0) x0 x1 (A : 'G^n),
-    x0 = 0 -> x1 = 0 ->  A = 0 ->insert2F H x0 x1 A = 0.
+    x0 = 0 -> x1 = 0 ->  A = 0 -> insert2F H x0 x1 A = 0.
 Proof. move=>> HA H0 H1; rewrite HA H0 H1; apply insert2F_zero. Qed.

 Lemma skipF_zero_compat :

--- a/Algebra/Monoid/Monoid_sum.v
+++ b/Algebra/Monoid/Monoid_sum.v
@@ -202,9 +202,9 @@ Lemma sum_splitF :
  forall {n1 n2} (u : 'G^(n1 + n2)), sum u = sum (firstF u) + sum (lastF u).
 Proof. intros n1 n2 u; rewrite {1}(concatF_splitF u); apply sum_concatF. Qed.

-Lemma sum_skipF : forall {n} (u : 'G^n.+1) i0, sum u = u i0 + sum (skipF i0 u).
+Lemma sum_skipF : forall {n} i0 (u : 'G^n.+1), sum u = u i0 + sum (skipF i0 u).
 Proof.
-intros n u i0.
+intros n i0 u.
 rewrite -(sum_castF (ordS_splitS i0)) sum_splitF sum_ind_r.
 rewrite -(sum_castF (ord_split i0)) sum_splitF.
 rewrite plus_assoc (plus_comm (u i0) _).
@@ -215,94 +215,93 @@ rewrite lastF_skipF; easy.
 Qed.

 Lemma sum_skipF_compat :
-  forall {n} (u v : 'G^n.+1) i0,
+  forall {n} i0 (u v : 'G^n.+1),
    u i0 = v i0 -> sum (skipF i0 u) = sum (skipF i0 v) -> sum u = sum v.
 Proof.
-intros n u v i0 H0 H1; rewrite !(sum_skipF _ i0) H0; apply plus_compat_l; easy.
+intros n i0 u v H0 H1; rewrite !(sum_skipF i0) H0; apply plus_compat_l; easy.
 Qed.

 Lemma sum_skipF_ex :
-  forall {n} u0 (u1 : 'G^n) i0,
+  forall {n} i0 u0 (u1 : 'G^n),
    exists u, sum u = u0 + sum u1 /\ u i0 = u0 /\ skipF i0 u = u1.
 Proof.
-intros n u0 u1 i0; destruct (skipF_ex i0 u0 u1) as [u [Hu0 Hu1]].
+intros n i0 u0 u1; destruct (skipF_ex i0 u0 u1) as [u [Hu0 Hu1]].
 exists u; repeat split; try easy; rewrite -Hu0 -Hu1; apply sum_skipF.
 Qed.

-Lemma sum_one : forall {n} (u : 'G^n.+1) i0, skipF i0 u = 0 -> sum u = u i0.
+Lemma sum_one : forall {n} i0 (u : 'G^n.+1), skipF i0 u = 0 -> sum u = u i0.
 Proof.
 intros; erewrite sum_skipF, sum_zero_compat; try apply plus_zero_r; easy.
 Qed.

 Lemma sum_skip_zero :
-  forall {n} {u : 'G^n.+1} i0, u i0 = 0 -> sum u = sum (skipF i0 u).
+  forall {n} i0 {u : 'G^n.+1}, u i0 = 0 -> sum u = sum (skipF i0 u).
 Proof.
 move=>> Hi0; rewrite -(plus_zero_l (sum (skipF _ _))) -Hi0; apply sum_skipF.
 Qed.

 Lemma sum_skip2F :
-  forall {n} (u : 'G^n.+2) {i0 i1} (H : i1 <> i0),
+  forall {n} {i0 i1} (H : i1 <> i0) (u : 'G^n.+2),
    sum u = u i0 + u i1 + sum (skip2F H u).
 Proof.
-intros n u i0 i1 H.
-rewrite (sum_skipF _ i0) -plus_assoc; f_equal.
-rewrite (sum_skipF _  (insert_ord H)) skip2F_correct; f_equal.
+intros n i0 i1 H u.
+rewrite (sum_skipF i0) -plus_assoc; f_equal.
+rewrite (sum_skipF (insert_ord H)) skip2F_correct; f_equal.
 rewrite skipF_correct; easy.
 Qed.

 Lemma sum_two :
-  forall {n} (u : 'G^n.+2) {i0 i1 : 'I_n.+2} (H : (i1 <> i0)%nat),
+  forall {n} {i0 i1 : 'I_n.+2} (H : i1 <> i0) (u : 'G^n.+2),
    skip2F H u = 0 -> sum u = u i0 + u i1.
 Proof.
 move=>> H; erewrite sum_skip2F, sum_zero_compat. apply plus_zero_r. apply H.
 Qed.

 Lemma sum_insertF :
-  forall {n} (u : 'G^n) x0 i0, sum (insertF i0 x0 u) = x0 + sum u.
+  forall {n} i0 x0 (u : 'G^n), sum (insertF i0 x0 u) = x0 + sum u.
 Proof.
 intros; erewrite sum_skipF; rewrite -> insertF_correct_l, skipF_insertF; easy.
 Qed.

-Lemma sum_insert0F : forall {n} (u : 'G^n) i0, sum (insert0F i0 u) = sum u.
+Lemma sum_insert0F : forall {n} i0 (u : 'G^n), sum (insert0F i0 u) = sum u.
 Proof. intros; rewrite sum_insertF plus_zero_l; easy. Qed.

 Lemma sum_insert2F :
-  forall {n} (u : 'G^n) x0 x1 {i0 i1} (H : i1 <> i0),
+  forall {n} {i0 i1} (H : i1 <> i0) x0 x1 (u : 'G^n),
    sum (insert2F H x0 x1 u) = x0 + x1 + sum u.
 Proof. intros; rewrite insert2F_correct 2!sum_insertF; apply plus_assoc. Qed.

 Lemma sum_replaceF :
-  forall {n} (u : 'G^n.+1) x0 i0, u i0 + sum (replaceF i0 x0 u) = x0 + sum u.
+  forall {n} i0 x0 (u : 'G^n.+1), u i0 + sum (replaceF i0 x0 u) = x0 + sum u.
 Proof.
-intros n u x0 i0; rewrite replaceF_equiv_def_insertF sum_insertF (sum_skipF u i0).
+intros n i0 x0 u; rewrite replaceF_equiv_def_insertF sum_insertF (sum_skipF i0).
 rewrite 2!plus_assoc (plus_comm (u i0)); easy.
 Qed.

 Lemma sum_replace0F :
-  forall {n} (u : 'G^n.+1) i0,
+  forall {n} i0 (u : 'G^n.+1),
    u i0 + sum (replace0F i0 u) = u i0 + sum (skipF i0 u).
 Proof. intros; rewrite sum_replaceF -sum_skipF plus_zero_l; easy. Qed.

 Lemma sum_replace2F :
-  forall {n} (u : 'G^n.+2) x0 x1 {i0 i1},
-    i1 <> i0 -> u i0 + u i1 + sum (replace2F i0 i1 x0 x1 u) = x0 + x1 + sum u.
+  forall {n} {i0 i1} (H : i1 <> i0) x0 x1 (u : 'G^n.+2),
+    u i0 + u i1 + sum (replace2F i0 i1 x0 x1 u) = x0 + x1 + sum u.
 Proof.
-intros n u x0 x1 i0 i1 H; unfold replace2F.
+intros n i0 i1 H x0 x1 u; unfold replace2F.
 rewrite (plus_comm x0) -plus_assoc -(replaceF_correct_r x0 _ H).
 rewrite sum_replaceF plus_comm3_l sum_replaceF plus_assoc; easy.
 Qed.

 Lemma sum_replace2F_eq :
-  forall {n} (u : 'G^n.+2) x0 x1 {i0 i1},
-    i1 = i0 -> u i1 + sum (replace2F i0 i1 x0 x1 u) = x1 + sum u.
-Proof. intros; rewrite -> replace2F_correct_eq, sum_replaceF; easy. Qed.
+  forall {n} {i0 i1} (H : i1 = i0) x0 x1 (u : 'G^n.+2),
+    u i1 + sum (replace2F i0 i1 x0 x1 u) = x1 + sum u.
+Proof. intros; rewrite replace2F_correct_eq// sum_replaceF; easy. Qed.

 Lemma sum_permutF :
  forall {n} p (u : 'G^n), injective p -> sum (permutF p u) = sum u.
 Proof.
-intros n p u Hp; induction n as [| n].
-rewrite !sum_nil; easy.
-rewrite (sum_skipF (permutF _ _) ord0) (sum_skipF u (p ord0)); f_equal.
+intros n p u Hp; induction n as [| n]; [rewrite !sum_nil; easy |].
+rewrite (sum_skipF ord0) (sum_skipF (p ord0)); f_equal.
 rewrite skipF_permutF IHn; try apply skip_f_ord_inj; easy.
 Qed.

@@ -334,8 +333,8 @@ Qed.

 Lemma sum_itemF : forall {n} (x : G) i0, sum (itemF n i0 x) = x.
 Proof.
-intros [| n] x i0; [now destruct i0 |].
-unfold itemF; generalize (sum_replaceF (0 : 'G^n.+1) x i0).
+intros [| n] x i0; [now destruct i0 |]; unfold itemF.
+unfold itemF; generalize (sum_replaceF i0 x (0 : 'G^n.+1)).
 rewrite sum_zero plus_zero_l plus_zero_r; easy.
 Qed.

@@ -387,8 +386,8 @@ Proof.
 apply (nat_ind2 (fun m n =>
    forall u : 'G^{m,n}, sum (sum u) = sum (sum (flipT u)))).
 intros; rewrite 2!sum_nil; easy.
-move=>> H u; rewrite 2!(sum_skipF _ ord0) sum_plus sum_row H -sum_skipTc; easy.
-move=>> H u; rewrite 2!(sum_skipF _ ord0) sum_plus sum_col -H sum_skipTc; easy.
+move=>> H u; rewrite 2!(sum_skipF ord0) sum_plus sum_row H -sum_skipTc; easy.
+move=>> H u; rewrite 2!(sum_skipF ord0) sum_plus sum_col -H sum_skipTc; easy.
 Qed.

 (** Functions to Abelian monoid. *)
@@ -430,7 +429,7 @@ Lemma sum_skipF_equiv :
  forall {n} {u v : 'G^n.+1} {i0},
    sum u = sum v -> sum (skipF i0 u) = sum (skipF i0 v) <-> u i0 = v i0.
 Proof.
-intros n u v i0; rewrite !(sum_skipF _ i0) => H; split; intros H0;
+intros n u v i0; rewrite !(sum_skipF i0) => H; split; intros H0;
    [| apply plus_is_reg_equiv in HG2]; move: H; rewrite H0; apply HG2.
 Qed.

@@ -483,7 +482,7 @@ Lemma sum_nonneg_ub_R :
  forall {n} (u : 'R^n) i, (forall i, 0 <= u i) -> u i <= sum u.
 Proof.
 intros [| n] u i Hx; [now destruct i |].
-rewrite (sum_skipF _ i) -{1}(plus_zero_r (u i)); apply Rplus_le_compat;
+rewrite (sum_skipF i) -{1}(plus_zero_r (u i)); apply Rplus_le_compat;
    [apply Rle_refl | apply sum_nonneg_R].
 intros; unfold skipF; easy.
 Qed.
@@ -560,7 +559,7 @@ rewrite replaceF_correct_r; try easy.
 rewrite constF_correct; auto with arith.
 rewrite <- (Nat.add_0_l (sum _)).
 replace 0%nat with (constF n.+1 0%nat i) at 1 by easy.
-generalize (sum_replaceF (constF n.+1 0) (u i) i).
+generalize (sum_replaceF i (u i) (constF n.+1 0)).
 unfold plus; simpl; intros T; rewrite T.
 rewrite sum_constF_nat.
 rewrite Nat.mul_0_r; auto with zarith.

--- a/Algebra/Monoid/Monomial_order.v
+++ b/Algebra/Monoid/Monomial_order.v
@@ -244,11 +244,11 @@ Qed.
 Lemma br_sum_conn_equiv :
  forall {R : G -> G -> Prop},
    monomial_order R ->
-    forall {n} {u v : 'G^n.+1} {i0},
+    forall {n} {i0} {u v : 'G^n.+1},
      sum u = sum v ->
      R (u i0) (v i0) <-> R (sum (skipF i0 v)) (sum (skipF i0 u)).
 Proof.
-move=>> HR n u v i0; rewrite !(sum_skipF _ i0); apply br_plus_conn_equiv; easy.
+move=>> HR n i0 u v; rewrite !(sum_skipF i0); apply br_plus_conn_equiv; easy.
 Qed.

 (** About the [monomial_order] / [monomial_order_ns] compound properties. *)
@@ -1309,7 +1309,7 @@ Proof. intros; split; [apply graded_r_rev | apply graded_r]; easy. Qed.

 (* The proof depends on the plus regularity hypothesis HG2. *)
 Lemma graded_S_r_equiv :
-  forall R {n} (Rn : 'G^n -> 'G^n -> Prop) (x y : 'G^n.+1) i0,
+  forall R {n} (Rn : 'G^n -> 'G^n -> Prop) i0 (x y : 'G^n.+1),
    x i0 = y i0 -> sum x = sum y ->
    graded R Rn (skipF i0 x) (skipF i0 y) <-> Rn (skipF i0 x) (skipF i0 y).
 Proof. intros; apply graded_r_equiv, sum_skipF_equiv; easy. Qed.
@@ -1814,14 +1814,14 @@ assert (HG2' : @plus_is_reg_r G) by now apply (monomial_order_plus_is_reg_r R).
 rewrite grsymlex_S; apply or_iff_compat_l; apply H0; intros H1; split.
 (* *)
 move=> [[/eq_sym_equiv H2 H3] | H2]; [| easy]; apply graded_l.
-contradict H2; move: H1; rewrite !(sum_skipF _ ord0) H2; apply HG2'.
+contradict H2; move: H1; rewrite !(sum_skipF ord0) H2; apply HG2'.
 apply br_sum_conn_equiv; easy.
 (* *)
 intros H2; destruct (HG1 (x ord0) (y ord0)) as [H3 | H3].
 right; repeat split; easy.
 left; repeat split; [easy.. |].
 apply graded_l_rev, br_sum_conn_equiv in H2; [easy.. |].
-contradict H3; move: H1; rewrite !(sum_skipF _ ord0) H3; apply HG2'.
+contradict H3; move: H1; rewrite !(sum_skipF ord0) H3; apply HG2'.
 Qed.

 (* The proof depends on the plus regularity hypothesis HG2. *)
@@ -1852,14 +1852,14 @@ assert (HG2' : @plus_is_reg_r G) by now apply (monomial_order_plus_is_reg_r R).
 rewrite grevlex_S; apply or_iff_compat_l; apply H0; intros H1; split.
 (* *)
 move=> [[/eq_sym_equiv H2 H3] | H2]; [| easy]; apply graded_l.
-contradict H2; move: H1; rewrite !(sum_skipF _ ord_max) H2; apply HG2'.
+contradict H2; move: H1; rewrite !(sum_skipF ord_max) H2; apply HG2'.
 apply br_sum_conn_equiv; easy.
 (* *)
 intros H2; destruct (HG1 (x ord_max) (y ord_max)) as [H3 | H3].
 right; repeat split; easy.
 left; repeat split; [easy.. |].
 apply graded_l_rev, br_sum_conn_equiv in H2; [easy.. |].
-contradict H3; move: H1; rewrite !(sum_skipF _ ord_max) H3; apply HG2'.
+contradict H3; move: H1; rewrite !(sum_skipF ord_max) H3; apply HG2'.
 Qed.
No results found