proposition: Lemma nsum_p11h f: nat_ord_seq f -> \osup (fun_image (range f) odegree) = \0o -> ~ finite_set (nsupport f) -> n_sum f = omega0.
proof: Proof. move => ax sz fs. move: (ax) => [fgf df fo]. have ha i: natp i -> odegree (Vg f i) = \0o. move => iN. have vf: inc (odegree (Vg f i)) (fun_image (range f) odegree). by apply: funI_i; apply/(range_gP fgf); rewrite df; exists i. case: (emptyset_dichot (odegree (Vg f i))) => //. by move => [t ta]; move: (setU_i ta vf); rewrite sz => /in_set0. have hb i: natp i -> (Vg f i) <o omega0. move => iN; move: (ha i iN) => d0. have oi: ordinalp (Vg f i) by apply: fo; ue. case: (ozero_dichot oi); first by move ->; apply: olt_0omega. by move/ the_cnf_p4 => /proj2; rewrite d0 osucc_zero oopow1. apply: oleA. exact: (nsum_p11d ax indecomp_omega hb). by apply: nsum_p11g. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)