Algebra/Ring/Ring_FF_FT.v

@@ -29,12 +29,12 @@ COPYING file for more details.
  - [alt_ones n] is the [n]-family with values [1], [-1], [1]...;
  - [alt_ones_shift n] is the [n]-family with values [-1], [1], [-1]...
  Let [u : 'K^n].
- - [part1F u i0] is the [n+1]-family where the value [1 - sum u] is
+ - [part1F i0 u] is the [n+1]-family where the value [1 - sum u] is
    inserted in [u] at position [i0];
- - [part1F_0 u] is [part1F u ord0].
+ - [part1F0] is an abbreviation for [part1F ord0].
  Let [x : K].
  - [plusn n x] is the [sum] of [n] items equal to [x];
- - [plusn1 n] is [plusn n 1].
+ - [plusn1] is an abbreviation for [plusn^~ 1].
 
  - [alt_onesT m n] is the [(m,n)]-table with values [1] at location [(i,j)]
    when [i+j] is even, and [-1] otherwise.
@@ -65,9 +65,7 @@ Local Open Scope Group_scope.
 Local Open Scope Ring_scope.
 
 
-Section Ring_FF_Facts1a.
-
-(** Properties with the second identity element of rings (one). *)
+Section Ring_FF_Def.
 
 Context {K : Ring}.
 
@@ -77,8 +75,31 @@ Definition alt_ones {n} : 'K^n :=
 Definition alt_ones_shift {n} : 'K^n :=
   fun i => if Nat.Even_Odd_dec i then - (1 : K) else 1.
 
+Definition alt_onesT {m n} : 'K^{m,n} :=
+  fun i j => if Nat.Even_Odd_dec (i + j) then 1 else - (1 : K).
+
+Definition part1F {n} (i0 : 'I_n.+1) (u : 'K^n) : 'K^n.+1 :=
+  insertF i0 (1 - sum u) u.
+
+Definition plusn (n : nat) (x : K) : K := sum (constF n x).
+
+End Ring_FF_Def.
+
+
+Notation part1F0 := (part1F ord0).
+Notation plusn1 := (plusn^~ 1).
+
+
+Section Ring_FF_Facts1.
+
+Context {K : Ring}.
+
+(** Properties with the second identity element of rings (one). *)
+
+(** Properties of [alt_ones]. *)
+
 Lemma alt_ones_correct_even :
-  forall {n} (i : 'I_n), Nat.Even i -> alt_ones i = 1.
+  forall {n} (i : 'I_n), Nat.Even i -> alt_ones i = 1 :> K.
 Proof.
 intros n i Hi; unfold alt_ones; destruct (Nat.Even_Odd_dec i); simpl; try easy.
 exfalso; apply (Nat.Even_Odd_False i); easy.
@@ -100,14 +121,15 @@ exfalso; apply (Nat.Even_Odd_False i); easy.
 Qed.
 
 Lemma alt_ones_shift_correct_odd :
-  forall {n} (i : 'I_n), Nat.Odd i -> alt_ones_shift i = 1.
+  forall {n} (i : 'I_n), Nat.Odd i -> alt_ones_shift i = 1 :> K.
 Proof.
 intros n i Hi; unfold alt_ones_shift;
     destruct (Nat.Even_Odd_dec i); simpl; try easy.
 exfalso; apply (Nat.Even_Odd_False i); easy.
 Qed.
 
-Lemma alt_ones_eq : forall {n}, @alt_ones n = liftF_S (@alt_ones_shift n.+1).
+Lemma alt_ones_eq :
+  forall {n}, @alt_ones K n = liftF_S (@alt_ones_shift K n.+1).
 Proof.
 intros n; extF i; unfold liftF_S; destruct (Nat.Even_Odd_dec i).
 (* *)
@@ -119,7 +141,7 @@ rewrite lift_S_correct; apply Nat.Even_succ; easy.
 Qed.
 
 Lemma alt_ones_shift_eq :
-  forall {n}, @alt_ones_shift n = liftF_S (@alt_ones n.+1).
+  forall {n}, @alt_ones_shift K n = liftF_S (@alt_ones K n.+1).
 Proof.
 intros n; extF i; unfold liftF_S; destruct (Nat.Even_Odd_dec i).
 (* *)
@@ -131,7 +153,7 @@ rewrite lift_S_correct; apply Nat.Even_succ; easy.
 Qed.
 
 Lemma alt_ones_shift2 :
-  forall {n}, @alt_ones n = liftF_S (liftF_S (@alt_ones n.+2)).
+  forall {n}, @alt_ones K n = liftF_S (liftF_S (@alt_ones K n.+2)).
 Proof. intros; rewrite alt_ones_eq alt_ones_shift_eq; easy. Qed.
 
 Lemma ones_not_zero : forall {n}, nonzero_struct K -> (1 : 'K^n.+1) <> 0.
@@ -145,7 +167,7 @@ apply one_not_zero; easy.
 apply Even_0.
 Qed.
 
-Lemma sum_alt_ones_even : forall {n}, Nat.Even n -> sum (@alt_ones n) = 0.
+Lemma sum_alt_ones_even : forall {n}, Nat.Even n -> sum (@alt_ones K n) = 0.
 Proof.
 intros n [m Hm]; subst; induction m as [| m Hm]. apply sum_nil.
 rewrite -(sum_castF (nat_double_S _)).
@@ -153,11 +175,11 @@ rewrite 2!sum_ind_l; unfold castF at 1, liftF_S at 1, castF at 1.
 rewrite {1}alt_ones_correct_even; try apply Even_0;
     rewrite alt_ones_correct_odd; try apply Odd_1.
 rewrite plus_assoc plus_opp_r plus_zero_l.
-rewrite -(sum_eq (@alt_ones (2 * m)%coq_nat)); try easy.
+rewrite -(sum_eq (@alt_ones _ (2 * m)%coq_nat)); try easy.
 apply alt_ones_shift2.
 Qed.
 
-Lemma sum_alt_ones_odd : forall {n}, Nat.Odd n -> sum (@alt_ones n) = 1.
+Lemma sum_alt_ones_odd : forall {n}, Nat.Odd n -> sum (@alt_ones K n) = 1.
 Proof.
 intros n [m Hm]; subst; induction m as [| m Hm].
 rewrite sum_1; apply alt_ones_correct_even, Even_0.
@@ -166,12 +188,12 @@ rewrite 2!sum_ind_l; unfold castF at 1, liftF_S at 1, castF at 1.
 rewrite {1}alt_ones_correct_even; try apply Even_0;
     rewrite alt_ones_correct_odd; try apply Odd_1.
 rewrite plus_assoc plus_opp_r plus_zero_l.
-rewrite -(sum_eq (@alt_ones ((2 * m)%coq_nat.+1))).
+rewrite -(sum_eq (@alt_ones _ ((2 * m)%coq_nat.+1))).
 rewrite -(sum_castF (addn1_sym _)); easy.
 apply alt_ones_shift2.
 Qed.
 
-Lemma alt_ones_3_eq : @alt_ones 3 = tripleF 1 (- (1)) 1.
+Lemma alt_ones_3_eq : @alt_ones K 3 = tripleF 1 (- (1)) 1.
 Proof.
 extF i; destruct (ord3_dec i) as [[-> | ->] | ->].
 rewrite -> alt_ones_correct_even, tripleF_0; try apply Even_0; easy.
@@ -185,42 +207,29 @@ Proof. rewrite -alt_ones_3_eq; apply sum_alt_ones_odd, Odd_3. Qed.
 Lemma sum_alt_ones_3_invertible : invertible (sum (tripleF 1 (- (1 : K)) 1)).
 Proof. rewrite sum_alt_ones_3; apply invertible_one. Qed.
 
-Definition part1F {n} (u : 'K^n) (i0 : 'I_n.+1) : 'K^n.+1 :=
-  insertF i0 (1 - sum u) u.
+(** Properties of [part1F]. *)
 
 Lemma part1F_correct_0 :
-  forall {n} (u : 'K^n) i0 i, i = i0 -> part1F u i0 i = 1 - sum u.
+  forall {n} i0 i (u : 'K^n), i = i0 -> part1F i0 u i = 1 - sum u.
 Proof. move=>> ->; unfold part1F; rewrite insertF_correct_l; easy. Qed.
 
 Lemma part1F_correct_S :
-  forall {n} (u : 'K^n) {i0 i} (Hi : i <> i0),
-    part1F u i0 i = u (insert_ord Hi).
+  forall {n} {i0 i} (Hi : i <> i0) (u : 'K^n),
+    part1F i0 u i = u (insert_ord Hi).
 Proof. intros; apply insertF_correct_r. Qed.
 
-Lemma part1F_sum : forall {n} (u : 'K^n) i0, sum (part1F u i0) = 1.
+Lemma part1F_sum : forall {n} i0 (u : 'K^n), sum (part1F i0 u) = 1.
 Proof. intro; apply sum_insertF_baryc. Qed.
 
 Lemma part1F_Rg :
-  forall {n} (i0 : 'I_n.+1), Rg (part1F^~ i0) = fun u => sum u = 1.
+  forall {n} (i0 : 'I_n.+1), Rg (part1F i0) = fun u => sum u = (1 : K).
 Proof.
 intros n i0; apply subset_ext_equiv; split.
 intros _ [v _]; apply part1F_sum.
 intros u Hu; rewrite image_ex; exists (skipF i0 u); split; [easy |].
-unfold part1F; rewrite -Hu (sum_skipF _ i0) minus_plus_r insertF_skipF; easy.
+unfold part1F; rewrite -Hu (sum_skipF i0) minus_plus_r insertF_skipF; easy.
 Qed.
 
-End Ring_FF_Facts1a.
-
-
-Notation part1F0 := (part1F^~ ord0).
-
-
-Section Ring_FF_Facts1b.
-
-(** Properties with the second identity element of rings (one). *)
-
-Context {K : Ring}.
-
 Lemma part1F0_1_eq : forall (a : K), part1F0 (singleF a) = coupleF (1 - a) a.
 Proof.
 intros; extF i; destruct (ord2_dec i) as [-> | ->].
@@ -236,7 +245,72 @@ Lemma part1F0_sum_1_invertible :
   forall (a : K), invertible (sum (coupleF (1 - a) a)).
 Proof. intros; rewrite part1F0_sum_1; apply invertible_one. Qed.
 
-End Ring_FF_Facts1b.
+(** Properties of [plusn]. *)
+
+Lemma plusn_0_l : forall x : K, plusn 0 x = 0.
+Proof. intros; apply sum_nil. Qed.
+
+Lemma plusn_0_r : forall n, plusn n (0 : K) = 0.
+Proof. intros; apply sum_zero. Qed.
+
+Lemma plusn_1_l : forall x : K, plusn 1 x = x.
+Proof. intros; apply sum_1. Qed.
+
+Lemma plusn_2_l : forall x : K, plusn 2 x = x + x.
+Proof. intros; apply sum_2. Qed.
+
+Lemma plusn_2_1 : plusn 2 (1 : K) = 2.
+Proof. rewrite plusn_2_l; easy. Qed.
+
+Lemma plusn1_2 : plusn1 2%nat = 2 :> K.
+Proof. apply plusn_2_1. Qed.
+
+Lemma plusn_3_l : forall x : K, plusn 3 x = x + x + x.
+Proof. intros; apply sum_3. Qed.
+
+Lemma plusn_ind : forall n (x : K), plusn n.+1 x = x + plusn n x.
+Proof. intros; apply sum_ind_l. Qed.
+
+Lemma plusn_plus_l :
+  forall n1 n2 (x : K), plusn (n1 + n2) x = plusn n1 x + plusn n2 x.
+Proof. intros; unfold plusn; rewrite -concatF_constF sum_concatF; easy. Qed.
+
+Lemma plusn_plus_r :
+  forall n (x y : K), plusn n (x + y) = plusn n x + plusn n y.
+Proof.
+intros n x y; induction n as [| n Hn].
+rewrite !plusn_0_l plus_zero_l; easy.
+rewrite !plusn_ind Hn -(plus_assoc _ (plusn _ _)) (plus_assoc (plusn _ _))
+    (plus_comm (plusn _ _) y) -(plus_assoc y) -(plus_assoc x y); easy.
+Qed.
+
+Lemma plusn_assoc_l :
+  forall n1 n2 (x : K), plusn (n1 * n2)%coq_nat x = plusn n1 (plusn n2 x).
+Proof.
+intros n1 n2 x; induction n1 as [| n1 Hn1].
+rewrite Nat.mul_0_l !plusn_0_l; easy.
+replace (n1.+1 * n2)%coq_nat with ((n1 * n2)%coq_nat + n2)%coq_nat by lia.
+rewrite plusn_plus_l Hn1 plusn_ind plus_comm; easy.
+Qed.
+
+Lemma plusn_assoc_r :
+  forall n1 n2 (x : K), plusn (n1 * n2)%coq_nat x = plusn n2 (plusn n1 x).
+Proof. intros; rewrite -plusn_assoc_l; f_equal; auto with arith. Qed.
+
+Lemma plusn_mult : forall n (x y : K), plusn n (x * y) = plusn n x * y.
+Proof. intros; unfold plusn; rewrite -mult_sum_l; easy. Qed.
+
+Lemma plusn_eq : forall n (x : K), plusn n x = (plusn1 n) * x.
+Proof. intros n x; rewrite -plusn_mult mult_one_l; easy. Qed.
+
+Lemma plusn_zero_equiv :
+  forall n, plusn1 n = 0 :> K <-> forall x : K, plusn n x = 0.
+Proof.
+intros; split; intros Hn; try easy.
+intros; rewrite plusn_eq Hn mult_zero_l; easy.
+Qed.
+
+End Ring_FF_Facts1.
 
 
 Section Ring_FF_Facts2.
@@ -313,94 +387,6 @@ Proof. easy. Qed.
 End Ring_FF_Facts2.
 
 
-Section Ring_FF_Facts3.
-
-Definition plusn {K : Ring} (n : nat) (x : K) : K := sum (constF n x).
-Definition plusn1 (K : Ring) (n : nat) : K := plusn n 1.
-
-Context {K : Ring}.
-
-Lemma plusn1_eq : forall n, plusn1 K n = plusn n 1.
-Proof. easy. Qed.
-
-Lemma plusn_0_l : forall x : K, plusn 0 x = 0.
-Proof. intros; apply sum_nil. Qed.
-
-Lemma plusn_0_r : forall n, plusn n (0 : K) = 0.
-Proof. intros; apply sum_zero. Qed.
-
-Lemma plusn_1_l : forall x : K, plusn 1 x = x.
-Proof. intros; apply sum_1. Qed.
-
-Lemma plusn_2_l : forall x : K, plusn 2 x = x + x.
-Proof. intros; apply sum_2. Qed.
-
-Lemma plusn_2_1 : plusn 2 (1 : K) = 2.
-Proof. rewrite plusn_2_l; easy. Qed.
-
-Lemma plusn1_2 : plusn1 K 2 = 2.
-Proof. rewrite plusn1_eq plusn_2_1; easy. Qed.
-
-Lemma plusn_3_l : forall x : K, plusn 3 x = x + x + x.
-Proof. intros; apply sum_3. Qed.
-
-Lemma plusn_ind : forall n (x : K), plusn n.+1 x = x + plusn n x.
-Proof. intros; apply sum_ind_l. Qed.
-
-Lemma plusn_plus_l :
-  forall n1 n2 (x : K), plusn (n1 + n2) x = plusn n1 x + plusn n2 x.
-Proof. intros; unfold plusn; rewrite -concatF_constF sum_concatF; easy. Qed.
-
-Lemma plusn_plus_r :
-  forall n (x y : K), plusn n (x + y) = plusn n x + plusn n y.
-Proof.
-intros n x y; induction n as [| n Hn].
-rewrite !plusn_0_l plus_zero_l; easy.
-rewrite !plusn_ind Hn -(plus_assoc _ (plusn _ _)) (plus_assoc (plusn _ _))
-    (plus_comm (plusn _ _) y) -(plus_assoc y) -(plus_assoc x y); easy.
-Qed.
-
-Lemma plusn_assoc_l :
-  forall n1 n2 (x : K), plusn (n1 * n2)%coq_nat x = plusn n1 (plusn n2 x).
-Proof.
-intros n1 n2 x; induction n1 as [| n1 Hn1].
-rewrite Nat.mul_0_l !plusn_0_l; easy.
-replace (n1.+1 * n2)%coq_nat with ((n1 * n2)%coq_nat + n2)%coq_nat by lia.
-rewrite plusn_plus_l Hn1 plusn_ind plus_comm; easy.
-Qed.
-
-Lemma plusn_assoc_r :
-  forall n1 n2 (x : K), plusn (n1 * n2)%coq_nat x = plusn n2 (plusn n1 x).
-Proof. intros; rewrite -plusn_assoc_l; f_equal; auto with arith. Qed.
-
-Lemma plusn_mult : forall n (x y : K), plusn n (x * y) = plusn n x * y.
-Proof. intros; unfold plusn; rewrite -mult_sum_l; easy. Qed.
-
-Lemma plusn_eq : forall n (x : K), plusn n x = (plusn1 K n) * x.
-Proof. intros n x; rewrite -plusn_mult mult_one_l; easy. Qed.
-
-Lemma plusn_zero_equiv :
-  forall n, plusn1 K n = 0 <-> forall x : K, plusn n x = 0.
-Proof.
-intros; split; intros Hn; unfold plusn1; try easy.
-intros; rewrite plusn_eq Hn mult_zero_l; easy.
-Qed.
-
-End Ring_FF_Facts3.
-
-
-Section Ring_FT_Facts.
-
-(** Properties with the second identity element of rings (one). *)
-
-Context {K : Ring}.
-
-Definition alt_onesT {m n} : 'K^{m,n} :=
-  fun i j => if Nat.Even_Odd_dec (i + j) then 1 else - (1 : K).
-
-End Ring_FT_Facts.
-
-
 Section Ring_FF_R_Facts.
 
 Lemma ones_not_zero_R : forall {n}, (1 : 'R_Ring^n.+1) <> 0.

Algebra/Ring/Ring_charac.v

@@ -58,11 +58,11 @@ Section Ring_charac.
 
 Lemma ring_charac_EX :
   forall K : Ring,
-    { n | n <> 0%nat /\ plusn1 K n = 0 /\
-          forall p, p <> 0%nat -> (p < n)%coq_nat -> plusn1 K p <> 0 } +
-    { forall n, n <> 0%nat -> plusn1 K n <> 0 }.
+    { n | n <> 0%nat /\ plusn1 n = 0 :> K /\
+          forall p, p <> 0%nat -> (p < n)%coq_nat -> plusn1 p <> 0 :> K } +
+    { forall n, n <> 0%nat -> plusn1 n <> 0 :> K }.
 Proof.
-intros; pose (P n := n <> 0%nat /\ plusn1 K n = 0).
+intros; pose (P n := n <> 0%nat /\ plusn1 n = 0 :> K).
 destruct (LPO P (fun=> classic _)) as [[N HN] | H]; [left | right].
 (* *)
 apply ex_EX; destruct (dec_inh_nat_subset_has_unique_least_element P)
@@ -87,7 +87,7 @@ Definition is_field_not_charac_2 (K : Ring) : Prop :=
 Context {K : Ring}.
 
 Lemma ring_charac_0 :
-  ring_charac K = 0%nat <-> forall n, n <> 0%nat -> plusn1 K n <> 0.
+  ring_charac K = 0%nat <-> forall n, n <> 0%nat -> plusn1 n <> 0 :> K.
 Proof.
 unfold ring_charac;
     destruct ring_charac_EX as [[n [Hn0 [Hn1 Hn2]]] | ]; simpl; try easy.
@@ -98,7 +98,7 @@ Qed.
 Lemma ring_charac_S :
   forall n, ring_charac K = n.+1 <->
     plusn n.+1 (1 : K) = 0 /\
-    (forall p, p <> 0%nat -> (p < n.+1)%coq_nat -> plusn1 K p <> 0).
+    (forall p, p <> 0%nat -> (p < n.+1)%coq_nat -> plusn1 p <> 0 :> K).
 Proof.
 intros n; unfold ring_charac;
     destruct ring_charac_EX as [[m [Hm0 [Hm1 Hm2]]] | H];
@@ -133,13 +133,12 @@ intros [Hn1 Hn2] k; split.
 (* .. *)
 move=> /plusn_zero_equiv Hk0.
 generalize (Nat.div_mod_eq k n.+1); intros Hk1.
-rewrite Hk1 plusn1_eq plusn_plus_l plusn_assoc_r
-    Hn1 plusn_0_r plus_zero_l in Hk0.
+rewrite Hk1 plusn_plus_l plusn_assoc_r Hn1 plusn_0_r plus_zero_l in Hk0.
 apply NNPP_equiv; contradict Hk0; apply Hn2; try easy.
 apply Nat.mod_upper_bound; easy.
 (* .. *)
 move=> /Nat.Div0.div_exact Hk; apply plusn_zero_equiv; rewrite Hk; try lia.
-unfold plusn1; rewrite plusn_assoc_r Hn1 plusn_0_r; easy.
+rewrite plusn_assoc_r Hn1 plusn_0_r; easy.
 (* . *)
 intros Hn; split.
 apply plusn_zero_equiv, Hn, Nat.Div0.mod_same; easy.
@@ -175,11 +174,11 @@ assert (Hk1 : k mod 2 = 0%nat \/ k mod 2 = 1%nat)
     by now apply lt_2, Nat.mod_upper_bound.
 destruct Hk1 as [Hk1 | Hk1]; try easy; contradict Hk.
 generalize (Nat.div_mod_eq k 2); intros Hk2; rewrite Hk2.
-rewrite plusn1_eq plusn_plus_l plusn_assoc_r HK1 plusn_0_r plus_zero_l Hk1 plusn_1_l.
+rewrite plusn_plus_l plusn_assoc_r HK1 plusn_0_r plus_zero_l Hk1 plusn_1_l.
 apply one_not_zero; easy.
 (* . *)
 apply Nat.Div0.div_exact in Hk; try easy; rewrite Hk.
-rewrite plusn1_eq plusn_assoc_r HK1 plusn_0_r; easy.
+rewrite plusn_assoc_r HK1 plusn_0_r; easy.
 Qed.
 
 Lemma ring_not_charac_2 :
@@ -189,13 +188,12 @@ rewrite -iff_not_r_equiv not_or_not_r_equiv -nonzero_not_zero_struct_equiv.
 apply ring_charac_2.
 Qed.
 
-Lemma invertible_plusn :
+Lemma invertible_plusn_not_ring_charac :
   forall n, nonzero_struct K -> n <> 0%nat ->
-    invertible (plusn1 K n) -> ring_charac K <> n.
+    invertible (plusn1 n : K) -> ring_charac K <> n.
 Proof.
 intros n HK0 Hn HK1; contradict Hn; destruct n; try easy; contradict HK1.
-apply ring_charac_S in Hn; rewrite plusn1_eq (proj1 Hn).
-apply noninvertible_zero; easy.
+apply ring_charac_S in Hn; rewrite (proj1 Hn); apply noninvertible_zero; easy.
 Qed.
 
 End Ring_charac.
@@ -206,10 +204,16 @@ Section Ring_R_Facts.
 Lemma ring_charac_0_R : ring_charac R_Ring = 0%nat.
 Proof.
 apply ring_charac_0; intro; rewrite -contra_equiv.
-rewrite plusn1_eq; unfold plusn; rewrite sum_constF_R Rmult_1_r.
+unfold plusn; rewrite sum_constF_R Rmult_1_r.
 intros Hn; apply INR_eq; rewrite INR_0; easy.
 Qed.
 
+Lemma invertible_plusn1_R : forall n, n <> 0 -> invertible (plusn1 n : R).
+Proof.
+intros; unfold plusn; rewrite sum_ones_R;
+    apply invertible_equiv_R, not_0_INR; easy.
+Qed.
+
 Lemma is_field_not_charac_2_R : is_field_not_charac_2 R_Ring.
 Proof. split; [apply is_field_R | rewrite ring_charac_0_R; easy]. Qed.
 

Algebra/Ring/Ring_compl.v

@@ -564,12 +564,12 @@ Lemma invertible_sum_equiv :
 Proof. intros; rewrite sum_filter_n0F; easy. Qed.
 
 Lemma sum_insertF_baryc :
-  forall {n} (u : 'K^n) i0, sum (insertF i0 (1 - sum u) u) = 1.
+  forall {n} i0 (u : 'K^n), sum (insertF i0 (1 - sum u) u) = 1.
 Proof. intros; rewrite sum_insertF plus_minus_l; easy. Qed.
 
 Lemma invertible_sum_squeezeF :
-  forall {n} (u : 'K^n.+1) {i0 i1},
-    i1 <> i0 -> invertible (sum u) -> invertible (sum (squeezeF i0 i1 u)).
+  forall {n} {i0 i1} (H : i1 <> i0) (u : 'K^n.+1),
+    invertible (sum u) -> invertible (sum (squeezeF i0 i1 u)).
 Proof. intros; rewrite sum_squeezeF; easy. Qed.
 
 Lemma is_integral_contra :

Algebra/Ring/Ring_kron.v

@@ -159,7 +159,7 @@ Lemma kron_sum_l :
 Proof.
 intros [| n] p j.
 move=> /Nat.le_0_r H; subst; destruct j; easy.
-move=> /leP H; rewrite (sum_one _ (widen_ord H j));
+move=> /leP H; rewrite (sum_one (widen_ord H j));
     [apply kron_is_1; easy | apply kron_skipF_diag_r].
 Qed.
 
@@ -169,7 +169,7 @@ Lemma kron_sum_r :
 Proof.
 intros [| n] p i.
 move=> /Nat.le_0_r H; subst; destruct i; easy.
-move=> /leP H; rewrite (sum_one _ (widen_ord H i));
+move=> /leP H; rewrite (sum_one (widen_ord H i));
     [apply kron_is_1 | rewrite (kron_skipF_diag_l (widen_ord _ _))]; easy.
 Qed.
 

FEM/FE_LagP.v

@@ -322,9 +322,8 @@ Lemma Sigma_LagPd0_eq_from_ref :
     Sigma_LagPd0 vtx id0 p =
       Sigma_LagPd0 vtx_ref id0 (p \o (T_geom vtx)).
 Proof.
-intros; unfold Sigma_LagPd0, node_d0; rewrite comp_correct T_geom_am.
-do 2 apply f_equal; extF; apply eq_sym, T_geom_vtx.
-rewrite sum_ones_R; apply invertible_equiv_R, R_compl.INR_n0, S_pos.
+intros; unfold Sigma_LagPd0, node_d0 at 1;
+    rewrite comp_correct node_ref_d0_node; easy.
 Qed.
 
 (**
@@ -337,7 +336,7 @@ Lemma Sigma_LagPSdSk_eq_from_ref :
       Sigma_LagPSdSk k vtx_ref i (p \o (T_geom vtx)).
 Proof.
 intros; unfold Sigma_LagPSdSk.
-rewrite comp_correct -node_ref_node T_geom_node; easy.
+rewrite comp_correct -node_ref_node; easy.
 Qed.
 
 Variable d k : nat.

FEM/LagP_node.v

@@ -42,14 +42,14 @@ Local Open Scope Group_scope.
 Local Open Scope Ring_scope.
 
 
-Section Node_Facts.
+Section Nodes_Facts1.
 
 Context {d k : nat}.
 
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
- Def 1588, Eq (9.80), p. 97. *)
-Definition node_d0 (vtx : 'R^{d.+1,d}) : 'R^d := isobarycenter_ms vtx.
+ Lem 1604, p. 101. *)
+Definition node_d0 (vtx : 'R^{d.+1,d}) : 'R^d := T_geom vtx node_ref_d0.
 
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
@@ -57,6 +57,21 @@ Definition node_d0 (vtx : 'R^{d.+1,d}) : 'R^d := isobarycenter_ms vtx.
 Definition node (vtx : 'R^{d.+1,d}) (idk : 'I_(pbinom d k).+1) : 'R^d :=
   T_geom vtx (node_ref idk).
 
+(**
+ #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
+ Def 1588, Eq (9.80), p. 97. *)
+Lemma node_d0_eq : forall vtx, node_d0 vtx = isobarycenter_ms vtx.
+Proof.
+intro; unfold node_d0; rewrite node_ref_d0_eqF T_geom_am;
+    [rewrite T_geom_vtxF | apply invertible_plusn1_R]; easy.
+Qed.
+
+(**
+ #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
+ Lem 1599, p. 100. *)
+Lemma node_ref_d0_node : node_ref_d0 = node_d0 vtx_ref.
+Proof. unfold node_d0; extF; rewrite T_geom_ref; easy. Qed.
+
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
  Lem 1599, p. 100. *)
@@ -95,14 +110,10 @@ intros; unfold Hface, node; rewrite Im_equiv; [| apply T_geom_inj; easy].
 apply node_ref_Hface_ref_S; easy.
 Qed.
 
-Lemma T_geom_node :
-  forall (idk : 'I_(pbinom d k).+1), T_geom vtx (node_ref idk) = node vtx idk.
-Proof. easy. Qed.
-
-End Node_Facts.
+End Nodes_Facts1.
 
 
-Section Nodes_Facts3.
+Section Nodes_Facts2.
 
 (** We need a dimension which is structurally nonzero.
  We take d = d1.+1 with d1 : nat. *)
@@ -134,7 +145,7 @@ Proof.
 intros; unfold T_geom_Hface; rewrite comp_correct inj_Hface_ref_S_node_ref//.
 Qed.
 
-End Nodes_Facts3.
+End Nodes_Facts2.
 
 
 Section Nodes_d1.
@@ -210,7 +221,7 @@ Qed.
 End Sub_vertices_Facts1.
 
 
-Section Sub_node_Def.
+Section Sub_nodes_Def.
 
 Context {d : nat}.
 Variable k : nat.
@@ -224,18 +235,16 @@ Definition sub_node : 'I_(pbinom d k.-1).+1 -> 'R^d := node (sub_vtx k vtx).
 Lemma sub_nodeF : sub_node = mapF (T_geom (sub_vtx k vtx)) node_ref.
 Proof. easy. Qed.
 
-End Sub_node_Def.
+End Sub_nodes_Def.
 
 
-Section Sub_node_ref_Facts1.
+Section Sub_nodes_ref_Facts1.
 
 Context {d k : nat}.
 Hypothesis Hk : (1 < k)%coq_nat.
 
 Lemma sub_node_ref : sub_node k (@vtx_ref d) = node (sub_vtx_ref k).
-Proof.
-unfold sub_node; f_equal; extF i; unfold sub_vtx; rewrite T_geom_ref; easy.
-Qed.
+Proof. rewrite sub_vtx_refF; easy. Qed.
 
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
@@ -251,10 +260,10 @@ rewrite !node_ref_eqF scal_assoc div_eq mult_comm_R -mult_assoc mult_inv_r;
 rewrite mult_one_r; do 2 f_equal; apply Adk_previous_layer; easy.
 Qed.
 
-End Sub_node_ref_Facts1.
+End Sub_nodes_ref_Facts1.
 
 
-Section Sub_node_Facts1.
+Section Sub_nodes_Facts1.
 
 Context {d k : nat}.
 Hypothesis Hk : (1 < k)%coq_nat.
@@ -273,13 +282,13 @@ Lemma sub_node_eq :
   sub_node k vtx = widenF (pbinomS_monot_pred d k) (node vtx).
 Proof.
 rewrite -T_geom_sub_nodeF sub_node_ref_eq// -widenF_mapF.
-f_equal; extF; rewrite mapF_correct -node_ref_node T_geom_node; easy.
+f_equal; extF; rewrite mapF_correct -node_ref_node; easy.
 Qed.
 
-End Sub_node_Facts1.
+End Sub_nodes_Facts1.
 
 
-Section Sub_node_Facts2.
+Section Sub_nodes_Facts2.
 
 Context {d : nat}.
 Context {vtx : 'R^{d.+1,d}}.
@@ -297,4 +306,4 @@ rewrite Adk_last_layer;[| easy | apply S_pos].
 rewrite Nat.nle_gt; simpl; apply /ltP; easy.
 Qed.
 
-End Sub_node_Facts2.
+End Sub_nodes_Facts2.

FEM/LagP_node_ref.v

@@ -41,20 +41,31 @@ Local Open Scope Group_scope.
 Local Open Scope Ring_scope.
 
 
-Section Node_ref_Facts1.
+Section Nodes_ref_Facts1.
 
 Context {d k : nat}.
 
+(**
+ #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
+ Lem 1601, Eq (9.93), p. 101. *)
+Definition node_ref_d0 : 'R^d := fun=> / INR d.+1.
+(* = constF d (/ INR d.+1). *)
+
+Lemma node_ref_d0_eqF : node_ref_d0 = isobarycenter_ms vtx_ref.
+Proof.
+rewrite isobaryc_ms_eq; [| apply invertible_plusn1_R; easy].
+unfold plusn; rewrite sum_ones_R vtx_ref_sum scal_ones//.
+Qed.
+
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
  Lem 1601, Eq (9.94), p. 101.#<BR>#
- This definition uses total function [inv].
+ This definition uses total function [inv] (via [div]).
  It will be used for k>0 only.
- The specific definition for k=0 is [node_d0], for any [vtx]. *)
+ The specific definition for k=0 is [node_ref_d0]. *)
 Definition node_ref (idk : 'I_(pbinom d k).+1) : 'R^d :=
   fun i => INR (Adk d k idk i) / INR k.
-(*  scal (/ INR k) (mapF INR (Adk d k idk)).*)
-(*  mapF (scal (/ INR k) (mapF INR)) (Adk d k).*)
+(* = mapF (scal (/ INR k) (mapF INR)) (Adk d k).*)
 
 Lemma node_ref_eqF :
   forall idk, node_ref idk = scal (/ INR k) (mapF INR (Adk d k idk)).
@@ -107,10 +118,10 @@ Lemma node_ref_Hface_ref_S :
     Hface_ref i (node_ref idk) <-> Adk d k idk (lower_S Hi) = O.
 Proof. intros; rewrite Hface_ref_S_eq node_ref_ASdki; easy. Qed.
 
-End Node_ref_Facts1.
+End Nodes_ref_Facts1.
 
 
-Section Node_ref_Facts2.
+Section Nodes_ref_Facts2.
 
 (** We need a dimension which is structurally nonzero.
  We take d = d1.+1 with d1 : nat. *)
@@ -145,10 +156,10 @@ apply (scal_reg_r _ Hk1); rewrite !scal_assoc mult_inv_r// !scal_one_l//.
 rewrite -mapF_insert0F; [easy | apply INR_0].
 Qed.
 
-End Node_ref_Facts2.
+End Nodes_ref_Facts2.
 
 
-Section Node_ref_d1.
+Section Nodes_ref_d1.
 
 Context {d : nat}.
 
@@ -168,14 +179,13 @@ Qed.
 Lemma node_vtx_ref_d1 : node_ref = castF (eq_sym (pbinomS_1_r d)) vtx_ref.
 Proof. intros; rewrite eq_sym_equiv -castF_sym_equiv -vtx_node_ref_d1//. Qed.
 
-End Node_ref_d1.
+End Nodes_ref_d1.
 
 
 Section Sub_vertices_ref_Def.
 
 Context {d : nat}.
 Variable k : nat.
-Variable vtx : 'R^{d.+1,d}.
 
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#

FEM/geom_transf_affine.v

@@ -304,9 +304,7 @@ Let pi_d_inv_inj := f_inv_inj pi_d_bij.
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
  Lem 1586, p. 96. *)
 Lemma T_geom_permutF_bij : bijective (T_geom_permutF vtx pi_d).
-Proof.
-apply T_geom_bij, aff_indep_permutF_equiv; [ apply injF_bij |]; easy.
-Qed.
+Proof. apply T_geom_bij, aff_indep_permutF; easy. Qed.
 
 Definition T_geom_permutF_inv : 'R^d -> 'R^d := f_inv (T_geom_permutF_bij).
 

FEM/monomial.v

@@ -195,7 +195,7 @@ Lemma powF_P_one :
     powF_P L B = pow (B k) a.
 Proof.
 intros d B L a k HL; destruct d; [destruct k; easy |].
-unfold powF_P; rewrite (prod_R_singl _ k).
+unfold powF_P; rewrite (prod_R_singl k).
 rewrite HL powF_correct; f_equal; apply itemF_correct_l; easy.
 (* Warning: the multiplicative identity element of R_mul is displayed here as 0! *)
 rewrite -powF_skipF HL skipF_itemF_diag.

FEM/multi_index.v

@@ -78,7 +78,7 @@ now apply Nat.eq_le_incl.
 apply nat_add_sub_r.
 rewrite <- H.
 rewrite -skipF_first.
-apply (sum_skipF alpha ord0).
+apply (sum_skipF ord0 alpha).
 (* *)
 unfold Slice_op; extF i; unfold castF; simpl.
 case (Nat.eq_0_gt_0_cases i); intros Hi.
@@ -325,8 +325,8 @@ Proof.
 intros n A B i H1 H2.
 apply Nat.add_lt_mono_l with (A i).
 apply Nat.le_lt_trans with (sum A).
-rewrite (sum_skipF A i); unfold plus; simpl; auto with arith.
-rewrite H1; rewrite (sum_skipF B i).
+rewrite (sum_skipF i A); unfold plus; simpl; auto with arith.
+rewrite H1; rewrite (sum_skipF i B).
 unfold plus; simpl.
 apply Nat.add_lt_mono_r; auto with arith.
 Qed.

FEM/poly_LagPd1_ref.v

@@ -71,6 +71,12 @@ fun_ext2; unfold liftF_S;
     rewrite (vtx_ref_S (lift_S_not_first _)) lower_lift_S; easy.
 Qed.
 
+Lemma vtx_ref_sum : sum vtx_ref = 1.
+Proof.
+rewrite sum_ind_l vtx_ref_0// plus_zero_l vtx_ref_SF.
+extF; rewrite fct_sum_eq kron_sum_l; easy.
+Qed.
+
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
  Lem 1436, p. 55. *)
@@ -347,7 +353,7 @@ intros j; rewrite Ker_equiv; apply LagPd1_ref_vtx_skipF.
 intros x_ref; move: (vtx_ref_aff_span x_ref) => /aff_span_EX [L [HL ->]].
 rewrite Ker_equiv.
 move: (LagPd1_ref_barycF_rev HL) => /extF_rev HL1; rewrite (HL1 i) => HLi.
-rewrite (baryc_skip_zero _ _ i)//; [apply Aff_span |].
+rewrite (baryc_skip_zero i)//; [apply Aff_span |].
 rewrite -(plus_zero_l (sum _)) -HLi -sum_skipF.
 1,2: apply invertible_eq_one; easy.
 Qed.