proposition: Lemma nsum_eventually_const f c: nat_ord_seq f -> \0o <o c -> (exists2 n, natp n & forall i, natp i -> n <=c i -> Vg f i = c) -> n_sum_rem f = c *o omega0.
proof: Proof. move => axf cp [n nN np]. case: (p_or_not_p (finite_set (nsupport f))) => fs. have sn: sub (nsupport f) Nat by apply: Zo_S. move: (finite_subset_Nat_bis sn fs) => [m] mN mp; ex_middle bad. move: (Nmax_p1 nN mN). set k := cmax _ _; move => [kN qb /cleNgt qc]. case: (inc_or_not k (nsupport f)); first by move/mp. case; apply:(Zo_i kN); rewrite (np _ kN qb); exact (nesym (proj2 cp)). move: (nsum_p10a axf fs) => [m mN mp]. move: (Nmax_p1 nN mN). set k := cmax _ _; move => [kN le1 le2]. move: (proj1 (mp k kN le2)). rewrite /n_sum_rem; Ytac0; move <-. move:Nat_order_wor => [wor sr]; move: (proj1 wor) => or. rewrite /n_sum_from_n/n_partial_sum. set shift := Lf (fun i => k +c i) Nat (Nat -s k). have sr1: sub (Nat -s k) (substrate Nat_order). by rewrite sr; apply: sub_setC. move: (iorder_osr or sr1). set r' := (induced_order Nat_order (Nat -s k)). move => [or2 sr2]. have axs: lf_axiom (csum2 k) Nat (Nat -s k). move => x xN; apply/setC_P; split; first by apply: NS_sum. by move => /(NltP kN) /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 kN yN); last by move/(NltP kN). move => xcp; move: (cdiff_pr xcp); move: (NS_diff k yN) => av bv. exists (y -c k) => //. 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 kN xN yN). by move => kk; apply /Nat_order_leP. pose fna := Lg Nat (fun i => Vg f (i+c k)). have fnag: fgraph fna by rewrite /fna; fprops. have dfna: domain fna = substrate Nat_order by rewrite /fna sr; aw. have fnax: [/\ fgraph fna, domain fna = substrate Nat_order & allf fna ordinalp]. split => //; rewrite /fna/allf; aw => x xN; rewrite LgV//; apply:(proj33 axf). by rewrite (proj32 axf); apply: NS_sum. move: (isum_p11 wor ois fnax). set w := Lg _ _. have ->: w = restr f (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 -> : ipartial_sum (restr f (substrate r')) r' (substrate r') = ipartial_sum f Nat_order (Nat -s k). have tt: sub (Nat -s k) (Nat -s k) by []. by rewrite /ipartial_sum sr2 /r' (double_restr _ tt) (iorder_trans _ tt). move <-. rewrite /ipartial_sum (iorder_substrate or). have ->: restr fna (substrate Nat_order) = cst_graph (substrate Nat_order)c. apply: Lg_exten; rewrite sr => i iN. rewrite /fna LgV//; apply: (np _ (NS_sum iN kN)). exact: (cleT le1 (csum_Mle0 i (CS_nat kN))). have is1: ordinal_o omega0 \Is Nat_order. apply: orderIS; rewrite - ord_omega_pr;apply: (ordinal_o_is wor). symmetry; exact: (oprod_pr1 (proj32_1 cp) OS_omega is1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)