proposition: Lemma sum_pred_eq : ∀ {I : eqType} (r : seq I) (P Q : pred I) (F : I → R), (∀ i : I, P i = Q i) → \sum_(i <- r | P i) F i = \sum_(i <- r | Q i) F i.
proof: Proof. intros I r P Q F ePQ. induction r as [| a r ihr]. - rewrite !big_nil. reflexivity. - rewrite !big_cons. case: ifP=> pa /=. + rewrite ePQ in pa. rewrite pa. rewrite ihr. reflexivity. + rewrite ePQ in pa. rewrite pa. apply ihr. Qed.
imports: Coq(Relation_Definitions RelationClasses Morphisms Utf8) Mon(FiniteProbabilities SPropMonadicStructures SpecificationMonads MonadExamples SPropBase) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples Commutativity GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum) Crypt(Axioms ChoiceAsOrd SubDistr Couplings Theta_dens Theta_exCP LaxComp FreeProbProg)