proposition: Lemma except_in_nsum_finite f: nat_ord_seq f -> exists2 n, natp n & forall i, inc i (except_in_nsums f) -> i <=c n.
proof: Proof. move =>[pq pb pc]. have aux k: natp k -> (except_in_nsum f) k -> exists2 n, natp n & forall m, natp m -> n <c m -> Vg f m <o Vg f k. rewrite /except_in_nsum; set E := Zo _ _ =>kN Ef. have qa: sub E Nat by apply: Zo_S. have ofk: ordinalp (Vg f k) by apply: pc; ue. have qb: nonempty E by exists k; apply:(Zo_i kN); apply: oleR. move: (finite_subset_Nat qa Ef qb) => [n /Zo_P [qc qd] qe]. exists n => // m mN lem. have oo: ordinalp (Vg f m) by apply: pc; ue. case: (oleT_el ofk oo) => // lt2. have /qe /cleNgt mE//: inc m E by apply: (Zo_i mN). rewrite /except_in_nsums;set E := Zo _ _. case: (emptyset_dichot E). move ->; exists \0c; [exact NS0 | by move => i /in_set0]. move => [t tE]. pose p x := exists2 k, inc k E & x = Vg f k. have pt: p (Vg f t) by exists t. have ot: ordinalp (Vg f t) by apply: pc; rewrite pb; move/Zo_S:tE. move: (least_ordinal4 ot pt); set u := least_ordinal _ _. move => [ou [k /Zo_P [kN kE] kv] etc]. move: (aux k kN kE) =>[n nN np]. exists n => // m mE; move: (mE) => /Zo_P [mN mp]. case: (NleT_el mN nN) => // lmn. case: (oltNge (np m mN lmn)). have pm: (p (Vg f m)) by exists m. have oo: ordinalp (Vg f m) by apply: pc; ue. by move: (etc _ oo pm);rewrite kv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)