kronecker.v now compiles

FEM/kronecker.v

@@ -107,6 +107,7 @@ case (lt_dec j n); intros Hn.*)
 
 
 (* old try *)
+(*
 intros j n a H.
 induction n; try easy.
 (* *)
@@ -134,7 +135,7 @@ erewrite Rmult_1_r; easy.
 rewrite sum_pn_zero; try easy.
 intros i Hi; unfold kronecker.
 case (eq_nat_dec i j); try lia.
-intro; erewrite Rmult_0_r; easy.
+intro; erewrite Rmult_0_r; easy.*)
 Admitted.
 
 Lemma kronecker_bigop_scal_out_l : forall n j (a : 'E^n), 
@@ -144,6 +145,7 @@ Proof.
 (* old try *)
 intros j n a H1.
 induction n; try easy.
+(*
 rewrite sum_pn_Sn.
 case (lt_dec j n); intros Hn.
 (*case1*)
@@ -153,7 +155,7 @@ admit.
 (*case2*)
 unfold kronecker at 2.
 case (eq_nat_dec n j); try lia.
-intros H2; replace (sum_pn _ _) with (@zero R_Ring).
+intros H2; replace (sum_pn _ _) with (@zero R_Ring).*)
 (*
 erewrite Rmult_0_r. 
 rewrite plus_zero_l; easy.  
@@ -169,13 +171,14 @@ Lemma kronecker_bigop_scal_in_r : forall n (i : 'I_n) (a : 'E^n),
   \big[plus/zero]_(j < n) scal (kronecker i j) (a j) = a i.
 Proof.
 (* old try *)
+(*
 intros i n a H.
 replace (fun j : nat => mult (a j) (kronecker i j)) with
   (fun j : nat => mult (a j) (kronecker j i)).
 apply kronecker_sum_scal_in_l; easy.
 apply functional_extensionality.
-intros j; f_equal; apply kronecker_sym.
-Qed.
+intros j; f_equal; apply kronecker_sym.*)
+Admitted.
 
 
 Lemma kronecker_bigop_scal_out_r : forall i n (a : 'E^n), 
@@ -183,26 +186,28 @@ Lemma kronecker_bigop_scal_out_r : forall i n (a : 'E^n),
   \big[plus%R/zero]_(j < n) scal (kronecker i j) (a j) = zero.
 Proof.
 (* old try *)
+(*
 intros i n a H1.
 replace (fun j : nat => mult (a j) (kronecker i j)) with
   (fun j : nat => mult (a j) (kronecker j i)).
 apply kronecker_sum_scal_out_l; easy.
 apply functional_extensionality.
-intros j; f_equal; apply kronecker_sym.
-Qed.
+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),
@@ -217,13 +222,14 @@ 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.
+Qed.*)
 Admitted.
 
 Lemma kronecker_bigop_prod : forall n (i j : 'I_n),