proposition: Lemma eqv_bigl I r (P1 P2 : pred I) (F : I -> X) : P1 =1 P2 -> \big[*%M/1]_(i <- r | P1 i) F i ≡ \big[*%M/1]_(i <- r | P2 i) F i.
proof: Proof. by move=> eqP12; rewrite -!(big_filter r) (eq_filter eqP12). Qed.
imports: HB(structures) Coq(RelationClasses Morphisms Relation_Definitions) mathcomp(all_ssreflect)