proposition: Lemma reindex_psum : (forall x, S x != 0 -> x \in P) -> {on P, bijective h} -> psum S = psum (fun x : U => S (h x)).
proof: Proof. move=> hP [hI h1 h2]; apply/(@reindex_psum_onto (some \o hI)) => //. + by move=> x Px /=; rewrite h2. + by move=> x Px /=; rewrite h1. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology