proposition: Lemma big_rel_seq : forall (I : eqType) (r : seq I) (P : pred I) F1 F2, (forall i, P i && (i \in r) -> Pr (F1 i) (F2 i)) -> Pr (\big[op1/idx1]_(i <- r | P i) F1 i) (\big[op2/idx2]_(i <- r | P i) F2 i).
proof: Proof. move=> I r P F1 F2 *; rewrite -> big_cond_seq. by rewrite -> (big_cond_seq (idx:=idx2)); apply big_rel. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops