proposition: Lemma all_sume_p4b f t: nat_ord_seq f -> inc t (permutations Nat) -> ( finite_set (nsupport f) <-> finite_set (nsupport (f_perm_t f t))).
proof: Proof. move:f t. suff aux f t: nat_ord_seq f -> inc t (permutations Nat) -> finite_set (nsupport f) -> finite_set (nsupport (f_perm_t f t)). move => f t ha hb; split; first by apply: aux. move => ff. move: (permutation_Si hb) => hb1. have ha1: (nat_ord_seq (f_perm_t f t)) by apply: f_perm_t_ax. move: (aux _ _ ha1 hb1 ff); congr finite_set; congr nsupport. move: ha =>[fgf df _]; rewrite /f_perm_t; apply: fgraph_exten; fprops; aw. done. move /permutationsP: hb =>[bt st tt]. hnf => x xn /=. have xtt: inc x (target t) by ue. move: (inverse_Vis bt xtt); rewrite st => txs. by rewrite !LgV// (inverse_V bt xtt). move => [fgf df fp] /permutationsP [bt st tt]. have fy := (proj1 (proj1 bt)). rewrite /nsupport /f_perm_t; set E := Zo _ _ ; set F := Zo _ _ => fse. have: sub F (fun_image E (Vf (inverse_fun t))). move => x /Zo_P [xN]; rewrite LgV// => h; apply/funI_P. move: (proj1 (proj1 bt)) => ft. have xst: inc x (source t) by ue. have txe: inc (Vf t x) E by apply: Zo_i h; Wtac. by ex_tac; rewrite inverse_V2. by move/sub_finite_set; apply; apply: finite_fun_image. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)