ipro -> power_measure

Author: affeldt-aist

classical/functions.v

@@ -2657,11 +2657,6 @@ Lemma fct_prodE (I : Type) (T : pointedType) (M : ringType) r (P : {pred I})
   \prod_(i <- r | P i) f i = fun x => \prod_(i <- r | P i) f i x.
 Proof. by apply/funext => ?; elim/big_rec2: _ => //= i y ? Pi <-. Qed.
 
-Lemma fct_prodE (I : Type) (T : pointedType) (M : comRingType) r (P : {pred I})
-    (f : I -> T -> M) (x : T) :
-  (\prod_(i <- r | P i) f i) x = \prod_(i <- r | P i) f i x.
-Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed.
-
 Lemma mul_funC (T : Type) {R : comSemiRingType} (f : T -> R) (r : R) :
   r \*o f = r \o* f.
 Proof. by apply/funext => x/=; rewrite mulrC. Qed.
@@ -2684,10 +2679,6 @@ Lemma prodrfctE (T : pointedType) (K : ringType) (s : seq (T -> K)) :
   \prod_(f <- s) f = (fun x => \prod_(f <- s) f x).
 Proof. exact: fct_prodE. Qed.
 
-Lemma prodrfctE (T : pointedType) (K : comRingType) (s : seq (T -> K)) :
-  \prod_(f <- s) f = (fun x => \prod_(f <- s) f x).
-Proof. by apply/funext => x;elim/big_ind2 : _ => // _ a _ b <- <-. Qed.
-
 Lemma natmulfctE (U : Type) (K : nmodType) (f : U -> K) n :
   f *+ n = (fun x => f x *+ n).
 Proof. by elim: n => [//|n h]; rewrite funeqE=> ?; rewrite !mulrSr h. Qed.