proposition: Lemma nsum_p12a f t: nat_ord_seq f -> inc t (permutations Nat) -> ~ finite_set (nsupport f) -> least_rem (n_sum (f_perm_t f t)) <=o least_rem (n_sum f).
proof: Proof. move => ax tp fs. move: (nsum_p9 ax fs) =>[n0 n0N remf]. move/(all_sume_p4b ax tp): fs => fts. move:(nsum_p9 (f_perm_t_ax ax tp) fts) =>[n1 n1N remtf]. move: (except_in_nsum_finite ax) => [n2 n2N n2p]. set E := fun_image (except_in_nsums f) (Vf (inverse_fun t)). have fse: finite_set E. apply: finite_fun_image; apply(except_in_nsum_finite2 ax). have sN: sub E Nat. move/permutationsP:tp => /inverse_bij_bp [[[ft _]_] st tt]. move => x/funI_P [i /Zo_S iN ->]; Wtac. move: (finite_subset_Nat_bis sN fse) =>[n3 n3N n3p]. pose bp i m n := [/\ natp n, m <c n & Vg f (Vf t i) <=o Vg f n]. have aux i m: natp i -> natp m -> n3 <=c i -> exists n, bp i m n. move => iN mN la. move/permutationsP:tp => [ bt st tt]. have tiN: natp (Vf t i) by rewrite /natp; Wtac; [ fct_tac | ue]. case: (inc_or_not (Vf t i) (except_in_nsums f)) => h. have sit: inc i (source t) by ue. have: inc i E by apply /funI_P;ex_tac; rewrite (inverse_V2 bt sit). by move=> /n3p /cltNge; case. set T := (Zo Nat (fun n => Vg f (Vf t i) <=o Vg f n)). case:(all_exists_dichot2 (fun n => m <c n) T); last first. by move => [n /Zo_P[qa qb] qc]; exists n. move => ha; case: h; apply: (Zo_i tiN). have hb: sub T (csucc m). move => s sT; apply/(NleP mN). have nN: natp s by move/ Zo_S: sT. by case: (NleT_el nN mN) => //; move:(ha _ sT). exact:(sub_finite_set hb (finite_set_nat (NS_succ mN))). pose b i m := intersection (Zo Nat (bp i m)). have aux2 i m: natp i -> natp m -> n3 <=c i -> bp i m (b i m). set Q:= (Zo Nat (bp i m)). have oQ: ordinal_set Q by move => x/Zo_S /OS_nat. move => ha hb hc; move: (aux _ _ ha hb hc) =>[n nn]. have neQ: nonempty Q by exists n; apply:Zo_i => //; case: nn. by move: (least_ordinal0 oQ neQ) => /proj32/Zo_hi. move: (cmax_p1 (CS_nat n1N) (CS_nat n3N)). set n13 := cmax n1 n3; move => [n13_la n13_lb]. have n13N: natp n13 by rewrite/n13/cmax/Gmax; Ytac h. pose ci := b n13 n0. pose c := induction_term (fun n => b (csucc (n +c n13))) ci. have c0: c \0o = ci by apply: induction_term0. move: (aux2 n13 n0 n13N n0N n13_lb); rewrite -/ci - c0 => c0p. have crec i: natp i -> c (csucc i) = b (csucc (i +c n13)) (c i). by move => iN; apply: induction_terms. have cic i: natp i -> bp (csucc (i +c n13)) (c i) (c (csucc i)). have qq:= (cleT n13_lb (cleS n13N)). move: i; apply: Nat_induction. rewrite (crec _ NS0) (csum0l (CS_nat n13N)); apply: aux2; fprops. exact: (proj31 c0p). move => i iN /proj31 Hrec; rewrite (crec _ (NS_succ iN)). have ll := (cleT qq (cleSS (Nsum_Mle0 (csucc i) n13N))). apply: aux2; fprops. move: (proj32 c0p) => c0_la. have c0_lb i: natp i -> (c i) <c c (csucc i) by move/cic; case. have cN i: natp i -> natp (c i). move => iN; case: (equal_or_not i \0c) => nz. by move: (proj31 c0p); rewrite nz. by move: (cpred_pr iN nz) => [/cic /proj31 sa ->]. have c0_lc i: natp i -> Vg f (Vf t (i +c n13)) <=o Vg f (c i). move => iN; case: (equal_or_not i \0c) => nz. by rewrite nz; move: (proj33 c0p); rewrite (csum0l (CS_nat n13N)). move: (cpred_pr iN nz) => [sa sb]. by move: (proj33 (cic _ sa)); rewrite - (csum_Sn _ sa) - sb. clear crec cic c0p. move:Nat_order_wor => [wor sr]. have or := proj1 wor. pose fna := Lg Nat (fun i => Vg f (Vf t (i+c n13))). pose fnb := Lg Nat (fun i => Vg f (c i)). have fnag: fgraph fna by rewrite /fna; fprops. have fnbg: fgraph fnb by rewrite /fnb; fprops. have dfna: domain fna = substrate Nat_order by rewrite /fna sr; aw. have dfnb: domain fnb = substrate Nat_order by rewrite /fnb sr; aw. have fnab x: inc x (substrate Nat_order) -> Vg fna x <=o Vg fnb x. by rewrite /fna /fnb sr => xN; rewrite !LgV//; apply: c0_lc. move: (isum_p8 wor fnag fnbg dfna dfnb fnab) => le1. have fnax: [/\ fgraph fna, domain fna = substrate Nat_order & allf fna ordinalp]. by split => // x; rewrite dfna => /fnab /proj31. have: ipartial_sum fna Nat_order (substrate Nat_order) = ipartial_sum (f_perm_t f t) Nat_order (Nat -s n13). set shift := Lf (fun i => n13 +c i) Nat (Nat -s n13). have sr1: sub (Nat -s n13) (substrate Nat_order). by rewrite sr; apply: sub_setC. move: (iorder_osr or sr1). set r' := (induced_order Nat_order (Nat -s n13)). move => [or2 sr2]. have axs: lf_axiom (csum2 n13) Nat (Nat -s n13). move => x xN; apply/setC_P; split; first by apply: NS_sum. by move => /(NltP n13N) /cltNge; case; apply: csum_M0le; fprops. have bsh: bijection shift. apply: lf_bijective => //. by move => x y xN yhN; apply:csum_eq2l. move => y /setC_P [yN xl]. case: (NleT_el n13N yN); last by move/(NltP n13N). move => xcp; move: (cdiff_pr xcp); move: (NS_diff n13 yN) => av bv. exists (y -c n13) => //. have ois : order_isomorphism shift Nat_order r'. split => //; first by split => //; rewrite/shift; aw. hnf; rewrite /shift; aw => x y xN yN; rewrite !LfV//. move:(axs x xN) (axs y yN) => xs ys. split. move /Nat_order_leP =>[_ _ lexy]; apply/(iorder_gle0P _ xs ys). apply/Nat_order_leP; split => //; fprops. by apply: csum_Meqle. move/(iorder_gle0P _ xs ys)=> /Nat_order_leP/proj33 /(csum_le2l n13N xN yN). by move => kk; apply /Nat_order_leP. rewrite (@isum_p11 fna Nat_order r' shift wor ois fnax). set w := Lg _ _. have ->: w = restr (f_perm_t f t) (substrate r'). apply: Lg_exten; rewrite sr2 => x xs. have xts: inc x (target shift) by rewrite /shift; aw. move: (inverse_V bsh xts). move: (inverse_Vis bsh xts); rewrite {2}/shift; aw. set y := (Vf (inverse_fun shift) x) => yN. rewrite /shift LfV// => eqa. move/setC_P : xs => [xN _]. by rewrite /fna /f_perm_t !LgV// csumC eqa. have tt: sub (Nat -s n13) (Nat -s n13) by []. by rewrite /ipartial_sum sr2 (double_restr _ tt)/r' (iorder_trans _ tt). rewrite -/(n_partial_sum (f_perm_t f t) _) -/(n_sum_from_n _ _). rewrite (remtf _ n13N n13_la); move <-. apply: (oleT le1). clear le1 fnax fnab dfna fnag fna. set E1 := fun_image Nat c. have cmon1 i j: i <c j -> natp j -> c i <c c j. move => lij jN; move: j jN lij; apply: Nat_induction. by move/clt0. move => j jN Hrec; move/(cltSleP jN); move:(c0_lb j jN) => aux1. case/cle_eqVlt; first by move ->. move/Hrec => /proj1 xx. apply: (cle_ltT xx aux1). have cmon2 i j: i <=c j -> natp j -> c i <=c c j. move => /cle_eqVlt cp jN; case: cp => h. by rewrite h; apply: cleR; apply: CS_nat; apply: cN. by move: (proj1 (cmon1 i j h jN)). have sa: sub E1 (Nat -s n0). move => x /funI_P [i iN ->]; move: (cmon2 _ _ (cle0n iN) iN) => la. move: (clt_leT c0_la la) => lb. apply/setC_P; split; first by apply: cN. move/(NltP n0N); apply cleNgt; exact: (proj1 lb). suff ->:ipartial_sum fnb Nat_order (substrate Nat_order) = n_partial_sum f E1. rewrite - (remf n0 n0N (cleR (CS_nat n0N))). have sb: sub (Nat -s n0) (substrate Nat_order) by rewrite sr; apply:sub_setC. exact: (isum_p10 wor sa sb (nsum_p0 ax)). rewrite /n_partial_sum. pose cf := Lf c Nat E1. have axcf: lf_axiom c Nat E1 by move => x xN; apply: funI_i. have bcf: bijection cf. apply: lf_bijective => //; last by move => y /funI_P. move => u v uN vN eqa; case: (NleT_ell uN vN) => // lt. by move: (proj2 (cmon1 _ _ lt vN)). by move: (nesym (proj2 (cmon1 _ _ lt uN))). have axb: [/\ fgraph fnb, domain fnb = substrate Nat_order & allf fnb ordinalp]. split; fprops;hnf; rewrite /fnb; aw => x xN; rewrite LgV//. by apply: (proj33 ax); rewrite (proj32 ax); apply: cN. have sb: sub E1 (substrate Nat_order). by rewrite sr => x /sa /setC_P/proj1. move: (iorder_osr or sb). set r' := induced_order _ _; move =>[ort' sr']. have is2: order_isomorphism cf Nat_order r'. split => //; first by rewrite sr sr'; split; rewrite /cf; aw. hnf; rewrite /cf; aw => x y xN yN; rewrite !LfV//. move:(axcf x xN) (axcf y yN) => xs ys. split. move /Nat_order_leP =>[_ _ lexy]; apply/(iorder_gle0P _ xs ys). apply/Nat_order_leP; split;fprops. move/(iorder_gle0P _ xs ys) => /Nat_order_leP/proj33 ll. apply /Nat_order_leP; split => //. case: (NleT_el xN yN) => // ly. by move:(cltNge (cmon1 y x ly xN) ll). have ww: sub E1 E1 by []. rewrite (@isum_p11 fnb Nat_order r' cf wor is2 axb). rewrite /ipartial_sum sr' /r' (iorder_trans _ ww); f_equal. apply: Lg_exten => x xe1; aw; rewrite /fnb. have xs: inc x (target cf) by rewrite /cf; aw. move: (inverse_Vis bcf xs) (inverse_V bcf xs); rewrite {2} /cf; aw. by set y := Vf _ _ => yN; rewrite /cf ! LgV// LfV//; move ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)