proposition: Lemma eqv_big I (r:seq I) (P1 P2 : pred I) (F1 F2 : I -> X) : P1 =1 P2 -> (forall i, P1 i -> F1 i ≡ F2 i) -> \big[*%M/1]_(i <- r | P1 i) F1 i ≡ \big[*%M/1]_(i <- r | P2 i) F2 i.
proof: Proof. by move/eqv_bigl <-; move/eqv_bigr->. Qed.
imports: HB(structures) Coq(RelationClasses Morphisms Relation_Definitions) mathcomp(all_ssreflect)