proposition: Lemma nsum_p11j f q (r:= oopow q) : nat_ord_seq f -> \0o <o q -> (forall i, natp i -> Vg f i <o r) -> \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. move: (indecomp_prop4 oq) => ir. pose S := nsupport f. have hc i: natp i -> ~ inc i S -> odegree (Vg f i) = \0o. move => iN /Zo_P w; case:(equal_or_not (Vg f i) \0o). by move ->; rewrite odegree_zero. by move => h; case:w. have hd: forall i, natp i -> odegree (Vg f i) <o q. move => i iN; case: (inc_or_not i S) => eis; last by rewrite (hc _ iN eis). have oi: ordinalp (Vg f i) by apply: fo; ue. move/Zo_hi: eis => fnz. move: (OS_degree oi) => od. move: (ole_ltT (proj1 (the_cnf_p4 (ord_ne0_pos oi fnz))) (ha _ iN)). by move /(opow_Mo_ltP od oq). pose W z := fun_image z (fun i => odegree (Vg f i)). have aux n: natp n ->q = \osup (W (Nat -s n)). move => nN. move: (@funU_setC Nat n (fun i => odegree (Vg f i))). rewrite /= -/(W _) -/(W _); move =>[rq rb]. have rc: ordinal_set (W Nat). by move => t /funI_P [i /hd/proj31_1 iN ->]. have rd: sub (W Nat -s W (Nat -s n)) (W Nat) by move => t /setC_P[]. have re: finite_set (W Nat -s W (Nat -s n)). by apply:rb; apply: finite_set_nat. have rf x: inc x (W Nat) -> x <o q. by move => /funI_P [i /hd hh -> ]. have rg: q = \osup (W Nat). rewrite - hb; apply: f_equal; set_extens t. move/funI_P =>[v /(range_gP fgf)[i idf ->] ->]; apply: funI_i; ue. move/funI_P =>[i iN ->]; apply: funI_i; apply/(range_gP fgf). rewrite df; ex_tac. by move: (osup_Un rc rd re rf rg) ; rewrite - rq. case: (p_or_not_p (finite_set (nsupport f))) => fs. have fsu: sub (nsupport f) Nat by apply:Zo_S. move: (finite_subset_Nat_bis fsu fs)=> [n nN hn]. move: (aux n nN) => qn. have hh: ordinal_set (W (Nat -s n)). move => t /funI_P[i /setC_P/proj1 iN ->]; apply:OS_degree. by apply:fo; ue. move: qp; rewrite qn. move/(olt_sup hh) => [z /funI_P [i /setC_P[iN ini] ->] dv]. case: ini; apply/(NltP nN). case: (inc_or_not i (nsupport f)); first by move /hn. by move => ns; case: (nesym(proj2 dv)); move: (hc _ iN ns). move: (nsum_p10a axf fs) =>[n nN np]. move: (indecomp_prop3 (least_rem_p3 (nsum_ne axf fs))) => [ p op pv]. case: (oleT_el oq op); last first. have hh: ordinal_set (W (Nat -s n)). move => t /funI_P[i /setC_P/proj1 iN ->]; apply:OS_degree. by apply:fo; ue. rewrite (aux _ nN); move/(olt_sup hh) => [d /funI_P [i ii ->] ] la. move/Zo_P: ii => [iN /(NltP nN) lin]. case: (NleT_el nN iN) => // lein. have ov: ordinalp (Vg f i) by apply: fo; ue. case:(ozero_dichot ov) => vp. by move: la; rewrite vp odegree_zero => /olt0. move: (ole_ltT (proj1 (the_cnf_p4 vp)) (proj2 (np _ iN lein))). rewrite pv => /oltNge; case; exact: (proj1(opow_Mo_lt la)). move => lpq. move: (proj1 (np n nN (cleR (CS_nat nN)))); rewrite pv => eq1. move: (nsum_p11d axf ir ha) => eq2. move: (opow_Mo_le lpq) => eq3. move: (osum_M0le (OS_nsumb axf nN)(OS_nsumc axf nN)). rewrite - (nsum_p2 axf nN) eq1 => eq4. exact: (oleA eq2 (oleT eq3 eq4)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)