proposition: Lemma psum_pair_swap (S : T * U -> R) : summable S -> psum S = psum (fun y => psum (fun x => S (x, y))).
proof: Proof. move=> sblS; rewrite (partition_psum snd) //; apply/eq_psum. move=> y /=; pose P := [pred xy : T * U | xy.2 == y]. rewrite (reindex_psum (h := [eta pair^~ y]) (P := P)) //=. + case=> x' y' /=; rewrite mulf_eq0 => /norP[_]. by rewrite pnatr_eq0 eqb0 negbK /P inE => /eqP->. + by exists fst => // -[x' y'] /eqP /= <-. by apply/eq_psum=> x /=; rewrite eqxx mulr1. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology