The use of big_pred0_eq doesn't work.

FEM/kronecker.v

@@ -92,13 +92,58 @@ Section kronecker_bigop.
 
 Context {E : ModuleSpace R_Ring}.
 
+Lemma kronecker_bigop_l : forall n (j : 'I_n),
+  (*(j < n)%nat -> *)
+  \big[plus%R/zero]_(i < n) (kronecker i j) = 1.
+Proof.
+(* old try *)
+(*
+intros j n H1.
+replace (sum_pn (fun i : nat => kronecker i j) n) with
+  (sum_pn (fun i : nat => mult (one) (kronecker i j)) n).
+apply kronecker_sum_scal_in_l; easy.
+f_equal; apply functional_extensionality.
+intros i; rewrite mult_one_l; easy.
+*)
+Admitted.
+
+Lemma kronecker_bigop_r : forall n (i : 'I_n),
+  (*(i < n)%nat -> *)
+  \big[plus%R/zero]_(j < n) (kronecker i j) = 1.
+Proof.
+(*intros i n H1.
+replace (fun j : nat => kronecker i j) with
+  (fun j : nat => kronecker j i).
+apply kronecker_sum_l; easy.
+apply functional_extensionality.
+intros j; apply kronecker_sym.*)
+
+(* old try *)
+(*
+intros i n H1.
+replace (fun j : nat => kronecker i j) with
+  (fun j : nat => kronecker j i).
+apply kronecker_sum_l; easy.
+apply functional_extensionality.
+intros j; apply kronecker_sym.
+Qed.*)
+Admitted.
+
+End kronecker_bigop.
+
+Section kronecker_bigop_scal.
+
+Context {E : ModuleSpace R_Ring}.
+Variable I : Type.
+Variable P : pred I.
+
 Lemma kronecker_bigop_scal_in_l : forall n (j : 'I_n) (a : 'E^n),
   (* (j < n)%nat -> *)
   \big[plus/zero]_(i < n) scal (kronecker i j) (a i) = a j.
 Proof.
 intros n j a.
 induction n.
-erewrite <- big_pred0_eq.
+erewrite <- big_pred0_eq. 
 (*
 rewrite bigop_plus_0; easy.
 (* *)
@@ -195,44 +240,7 @@ apply functional_extensionality.
 intros j; f_equal; apply kronecker_sym.*)
 Admitted.
 
-Lemma kronecker_bigop_l : forall n (j : 'I_n),
-  (*(j < n)%nat -> *)
-  \big[plus%R/zero]_(i < n) (kronecker i j) = 1.
-Proof.
-(* old try *)
-(*
-intros j n H1.
-replace (sum_pn (fun i : nat => kronecker i j) n) with
-  (sum_pn (fun i : nat => mult (one) (kronecker i j)) n).
-apply kronecker_sum_scal_in_l; easy.
-f_equal; apply functional_extensionality.
-intros i; rewrite mult_one_l; easy.
-*)
-Admitted.
-
-Lemma kronecker_bigop_r : forall n (i : 'I_n),
-  (*(i < n)%nat -> *)
-  \big[plus%R/zero]_(j < n) (kronecker i j) = 1.
-Proof.
-(*intros i n H1.
-replace (fun j : nat => kronecker i j) with
-  (fun j : nat => kronecker j i).
-apply kronecker_sum_l; easy.
-apply functional_extensionality.
-intros j; apply kronecker_sym.*)
-
-(* old try *)
-(*
-intros i n H1.
-replace (fun j : nat => kronecker i j) with
-  (fun j : nat => kronecker j i).
-apply kronecker_sum_l; easy.
-apply functional_extensionality.
-intros j; apply kronecker_sym.
-Qed.*)
-Admitted.
-
-Lemma kronecker_bigop_prod : forall n (i j : 'I_n), 
+Lemma kronecker_bigop_scal : forall n (i j : 'I_n), 
   (i < n)%nat -> (j < n)%nat ->
   \big[plus%R/zero]_(k < n) scal (kronecker i k) (kronecker k j) = kronecker i j.
 Proof.
@@ -250,4 +258,4 @@ admit.
 Admitted.
 
 
-End kronecker_bigop.
\ No newline at end of file
+End kronecker_bigop_scal.
\ No newline at end of file