proposition: Lemma big_rel : forall I r (P : pred I) F1 F2, (forall i, (P i) -> 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 PrF. elim: r => //= i *; case Pi: (P i); auto. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops