proposition: Lemma eq_bigl_supp (r : seq I) (P1 : pred I) (P2 : pred I) (F : I -> R) : {in [pred x | F x != idx], P1 =1 P2} -> \big[op/idx]_(i <- r | P1 i) F i = \big[op/idx]_(i <- r | P2 i) F i.
proof: Proof. move=> P12; rewrite big_mkcond [RHS]big_mkcond; apply: eq_bigr => i _. by case: (eqVneq (F i) idx) => [->|/P12->]; rewrite ?if_same. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)