proposition: Lemma nsum_p11g f: nat_ord_seq f -> ~ finite_set (nsupport f) -> omega0 <=o n_sum f.
proof: Proof. move => axf fs. move: (nsum_p10a axf fs) =>[n nN np]. move: (proj1 (np n nN (cleR (CS_nat nN)))) => eq. move: (osum_M0le (OS_nsumb axf nN)(OS_nsumc axf nN)). rewrite - (nsum_p2 axf nN) eq; apply: oleT. move: (nsum_p11e axf); rewrite /n_sum_rem; Ytac0. move: (indecomp_prop3 (least_rem_p3 (nsum_ne axf fs))) => [p op ->]. case: (ozero_dichot op); first by move ->; rewrite oopow0. by move=> /oge1P /opow_Mo_le; rewrite oopow1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)