proposition: Lemma nsum_p12b f t: nat_ord_seq f -> inc t (permutations Nat) -> ~ finite_set (nsupport f) -> least_rem (n_sum (f_perm_t f t)) = least_rem (n_sum f).
proof: Proof. move => ha hb hc. apply: (oleA (nsum_p12a ha hb hc)). move/ (all_sume_p4b ha hb): hc => hc'. move: (f_perm_t_ax ha hb) => ha'. move:(permutation_Si hb) => hb'. move: (nsum_p12a ha' hb' hc'). set h := f_perm_t _ _; have -> //: h = f. move: ha =>[fgf df _]. rewrite /h/f_perm_t; apply: fgraph_exten; fprops; aw; first exact. move/permutationsP: hb =>[bt st tt]. move => i iN /=. have it: inc i (target t) by ue. move: (inverse_Vis bt it)(inverse_V bt it); rewrite st ; move=> ra rb. rewrite !LgV//; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)