proposition: Lemma eqd_big_mul n (P : pred 'I_n) (F1 F2 : 'I_n -> R) : (forall i, P i -> F1 i %= F2 i) -> \prod_(i | P i) F1 i %= \prod_(i | P i) F2 i.
proof: Proof. apply: (big_ind2 (@eqd R))=> // a b c d. exact: eqd_mul. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool Arith.Wf_nat) mathcomp(eqtype ssrnat div seq path) mathcomp(ssralg fintype perm tuple choice generic_quotient) mathcomp(matrix bigop zmodp mxalgebra poly) stronglydiscrete