proposition: Lemma nsum_p11i f q: nat_ord_seq f -> ordinalp q -> \osup (fun_image (range f) odegree) = q -> n_sum f <=o oopow (osucc q).
proof: Proof. move => axf oq sf; move: (OS_succ oq) => osq. move: (indecomp_prop4 osq) => iq. apply: (nsum_p11d axf iq) => i iN. move: (axf) => [fgf df fo]. have ov: ordinalp (Vg f i) by apply: fo; ue. case: (ozero_dichot ov); first by move ->; apply: oopow_pos. move/ the_cnf_p4 => /proj2 => h; apply:(olt_leT h). apply/opow_Mo_le; apply/oleSSP; rewrite - sf; apply: ord_sup_ub. move => t /funI_P [v /(range_gP fgf) [j jN ->] ->]. by apply: OS_degree; apply: fo. by apply: funI_i; apply/(range_gP fgf); rewrite df; exists i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)