proposition: Lemma nsum_p11k f q (r:= oopow (osucc q)) : nat_ord_seq f -> \0o <o q -> ~ (finite_set (Zo Nat (fun i => oopow q <=o Vg f i))) -> \osup (fun_image (range f) odegree) = q -> n_sum f = r.
proof: Proof. move => axf qp ha hb. move: (axf) => [fgf df fo]. move: (proj32_1 qp) => oq. have ooq := OS_oopow oq. move: (indecomp_prop4 (OS_succ oq)) => ir. apply: oleA; first by apply: nsum_p11i. move: ha; set A := Zo _ _ => nfA. set s1 := ipartial_sum f Nat_order (substrate Nat_order). move: (nsum_p0 axf) => ax. move:Nat_order_wor => [wor sr]. have <-: s1 = n_sum f. by rewrite (nsum_p1 axf) /n_partial_sum /s1 sr. set s2 := ipartial_sum f Nat_order A. have saN: sub A Nat by apply: Zo_S. have sas: sub A (substrate Nat_order) by rewrite sr. have ra: s2 <=o s1 by apply:(isum_p10 wor sas (@sub_refl _) ax). move: (induced_wor wor sas) (iorder_sr (proj1 wor) sas). set r1 := induced_order _ _ => wor1 sr1. set s3 := ipartial_sum (Lg A (fun _ => (oopow q))) Nat_order A. have rb: s3 <=o s2. set g := (Lg A (fun _ => (oopow q))). have pa: fgraph g by rewrite /g; fprops. have pb: fgraph (restr f A)by apply: restr_fgraph. have pc: domain g = substrate r1 by rewrite /g; aw. have pd: domain (restr f A) = substrate r1 by aw. have pe x: inc x (substrate r1) -> Vg g x <=o Vg (restr f A) x. by rewrite /g sr1 => tA; rewrite !LgV//; move/Zo_hi: tA. have AA : sub A A by []. move: (isum_p8 wor1 pa pb pc pd pe). by rewrite /s2 /s3 /ipartial_sum /r1 sr1 (iorder_trans _ AA) (double_restr ). move:(oleT rb ra). pose fA := (Lg A (fun _ : Set => oopow q)). have ->: s3 = ipartial_sum fA r1 (substrate r1). by rewrite /s3/ipartial_sum sr1 /r1 (iorder_trans _(@sub_refl A)). have axa: [/\ fgraph fA, domain fA = substrate r1 & allf fA ordinalp]. by rewrite /fA /allf; aw; split; fprops => x xA; rewrite LgV//. have is1: ordinal_o omega0 \Is Nat_order. apply: orderIS; rewrite - ord_omega_pr;apply: (ordinal_o_is wor). move:(proj2 (sub_nat_isomorphism saN) nfA)=>[g isg]. rewrite (isum_p11 wor1 isg axa). set fB := Lg _ _. move: (oprod_pr1 ooq OS_omega is1). rewrite - (oopow_succ oq) -/r => ->. rewrite /ipartial_sum (iorder_substrate (proj1 wor)). congr (osum Nat_order _ <=o s1). apply: Lg_exten => x xsr;rewrite /fB /fA !LgV//. move: isg =>[_ _ [bg sg tg] _]. by rewrite - sr1 /r1 - sg; apply: (inverse_Vis bg); rewrite tg. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)