proposition: Lemma sum_oneq_eq : ∀ {I : eqType} (r : seq I) (P : pred I) (F G : I → R), (∀ i : I, P i → F i = G i) → \sum_(i <- r | P i) F i = \sum_(i <- r | P i) G i.
proof: Proof. intros I r P F G eFG. induction r as [| a r ihr]. - rewrite !big_nil. reflexivity. - rewrite !big_cons. case: ifP=> pa /=. + rewrite eFG. 2: auto. rewrite ihr. reflexivity. + 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)