proposition: Lemma nsum_p11f f q: nat_ord_seq f -> ~ finite_set (nsupport f) -> ordinalp q -> n_sum f = oopow q -> n_sum_small_idx f = emptyset.
proof: Proof. move => axf fs oq sv. move: (indecomp_prop4 oq) => ir. move: (least_rem_p5 ir) => eqa. move: (nsum_p10a axf fs) =>[n nN np]. move: (proj1 (np n nN (cleR (CS_nat nN)))) => eq1. rewrite /n_sum_small_idx; Ytac0; apply/set0_P => i /Zo_P [iN]. move: (osum_M0le (OS_nsumb axf iN)(OS_nsumc axf iN)). rewrite - (nsum_p2 axf iN)sv eqa (nsum_p4 axf iN) => ea eb. move: (NS_succ iN) => siN; case: fs. have aux := (OS_nsumc axf siN). move : (osum_Mle0 (proj32 eb) aux) => ec. exact: (nsum_p6 axf siN (osum2_a_ab (proj31 ec) aux (oleA (oleT ea eb) ec))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)