proposition: Lemma nsum_p12c f t (g := f_perm_t f t) (rho := n_sum_rem f) (E := n_sum_small_idx f) (Eg := fun_image E (Vf (inverse_fun t))): nat_ord_seq f -> inc t (permutations Nat) -> [/\ finite_set E, n_sum f = (n_partial_sum f E) +o rho & n_sum g = (n_partial_sum g Eg) +o rho ].
proof: Proof. move => axf pt. set S:= nsupport f. set S':= nsupport g. move:(f_perm_t_ax axf pt) => axg. move/permutationsP: (pt) => [bt st tt]; move: (proj1 (proj1 bt)) => ft. have aux p: Zo Nat (fun i => p (Vg g i)) = fun_image (Zo Nat (fun i => p (Vg f i))) (Vf (inverse_fun t)). rewrite /g/f_perm_t; set_extens i. move => /Zo_P[iN]; rewrite LgV// => ha. have isf: inc i (source t) by ue. apply/funI_P; exists (Vf t i);first by apply: Zo_i => //; Wtac. by rewrite (inverse_V2 bt isf) . move/funI_P => [j /Zo_P [jN jv] ->]. have tj: inc j (target t) by ue. move:(inverse_Vis bt tj); rewrite st => ha. by apply (Zo_i ha); rewrite LgV// (inverse_V bt tj). have aux2 p: finite_set (Zo Nat (fun i => p (Vg g i))) <-> finite_set (Zo Nat (fun i => p (Vg f i))). apply: (iff_trans(card_finite_setP _)). apply: (iff_trans _ (iff_sym (card_finite_setP _))). have h: {inc Zo Nat (fun i => p (Vg f i)) &, injective (Vf (inverse_fun t))}. move => x y /Zo_S xN /Zo_S yN sv. have xtt: inc x (target t) by ue. have ytt: inc y (target t) by ue. by rewrite - (inverse_V bt xtt) sv (inverse_V bt ytt). by rewrite aux (cardinal_fun_image h). have eqa: S' = fun_image S (Vf (inverse_fun t)). apply: (aux (fun i => i <> \0o)). have sfs: finite_set S' <-> finite_set S. apply: (aux2 (fun i => i <> \0o)). have fsE: finite_set E by apply: nsum_p10c. have eqb: n_sum f = n_partial_sum f E +o rho by apply: (nsum_p10g axf). split => //. case: (p_or_not_p (finite_set S)) => fs. move/sfs: (fs) => fs'. rewrite /rho /Eg /E/ n_sum_small_idx /n_sum_rem; Ytac0; Ytac0. by rewrite - eqa; apply: nsum_p10f. move/sfs: (fs) => fs'. rewrite (nsum_p10g axg) -/g. have rc: least_rem (n_sum f) = rho by rewrite /rho /n_sum_rem;Ytac0. rewrite /n_sum_small_idx; Ytac0. rewrite /Eg. move: (nsum_p12b axf pt fs); rewrite rc -/g => ee. rewrite /n_sum_rem /E /n_sum_small_idx /n_sum_small_idx1; Ytac0; Ytac0. by rewrite ee rc - aux. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)