proposition: Lemma summable_pair_eq {A : choiceType} {B C : eqType} (f1 f3 : A -> B) (f2 f4 : A -> C) (h1 : realsum.summable (T:=A) (R:=R) (λ x, (f1 x == f3 x)%:R)) (h2 : realsum.summable (T:=_) (R:=R) (λ x, (f2 x == f4 x)%:R)) : realsum.summable (T:=_) (R:=R) (λ x, ((f1 x, f2 x) == (f3 x, f4 x))%:R).
proof: Proof. match goal with | |- realsum.summable ?f => eassert (f = _) as Hf end. { extensionality x. apply (destruct_pair_eq (a:= f1 x) (b:=f3 x) (c:= f2 x) (d := f4 x)). } rewrite Hf. apply realsum.summableM. all: assumption. Qed.
imports: Coq(Utf8) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) mathcomp(ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice reals distr seq all_algebra fintype realsum) extructures(ord fset fmap) Mon(SPropBase) Crypt(Prelude Axioms ChoiceAsOrd SubDistr Couplings RulesStateProb UniformStateProb UniformDistrLemmas StateTransfThetaDens StateTransformingLaxMorph choice_type pkg_core_definition pkg_notation pkg_tactics pkg_composition pkg_heap pkg_semantics pkg_lookup pkg_advantage pkg_invariants pkg_distr) Equations.Prop.DepElim Equations(Equations) Crypt(FreeProbProg)