proposition: Lemma reindex_psum_onto h' : (forall x, S x != 0 -> x \in P) -> (forall i, i \in P -> omap h (h' i) = Some i) -> (forall i, h i \in P -> h' (h i) = Some i) -> psum S = psum (fun x : U => S (h x)).
proof: Proof. move=> PS hO hP; rewrite !psum_sup_seq; congr sup; rewrite predeqE => x. split=> -[J uqJ ->] {x}; last first. exists [seq h j | j <- J & S (h j) != 0]. rewrite map_inj_in_uniq ?filter_uniq // => y1 y2. rewrite !mem_filter => /andP[nz_S1 _] /andP[nz_S2 _]. by move/(congr1 h'); rewrite !hP ?PS // => -[]. apply/eqP; rewrite big_map big_filter. rewrite (bigID (fun i => S (h i) == 0)) /= big1 ?add0r //. by move=> y /eqP->; rewrite normr0. have uqpJ: uniq (pmap h' [seq j | j <- J & S j != 0]). apply/(map_uniq (f := some)); rewrite pmapS_filter. rewrite map_inj_in_uniq ?filter_uniq // => [y1 y2|]; last first. by rewrite map_id filter_uniq. rewrite !map_id !mem_filter => /andP[h'1 h1] /andP[h'2 h2]. case/andP: h1 => h1 _; case/andP: h2 => h2 _. by move/(congr1 (omap h)); rewrite !hO ?PS // => -[]. exists (pmap h' [seq j | j <- J & S j != 0]) => //. apply/eqP; rewrite -(big_map h predT \`|S|) (bigID [pred j | S j == 0]) /=. rewrite big1 ?add0r => [i /eqP->|]; first by rewrite normr0. rewrite -big_filter; apply/eqP; apply/perm_big/uniq_perm. + by rewrite filter_uniq. + rewrite map_inj_in_uniq // !map_id => y1 y2 h1 h2. move/(congr1 h'); rewrite !hP ?PS //; last by case. * move: h1; rewrite mem_pmap => /mapP[x1]. rewrite mem_filter => /andP[nz_Sx1 _] /(congr1 (omap h)) /=. by rewrite hO ?PS // => -[->]. * move: h2; rewrite mem_pmap => /mapP[x2]. rewrite mem_filter => /andP[nz_Sx2 _] /(congr1 (omap h)) /=. by rewrite hO ?PS // => -[->]. move=> x; rewrite !mem_filter; apply/andP/idP. + case=> nzSx Jx; apply/mapP; move/(_ x (PS _ nzSx)): hO. case E: (h' x) => [u|] //= -[xE]; exists u => //. rewrite mem_pmap; apply/mapP; exists x => //. by rewrite map_id mem_filter nzSx. + case/mapP=> u; rewrite mem_pmap => /mapP[t]; rewrite map_id. rewrite mem_filter=> /andP[h1 h2] /(congr1 (omap h)) /=. by rewrite hO ?PS // => -[->] ->; split. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology