proposition: Lemma nsum_p11d f r: nat_ord_seq f -> indecomposable r -> (forall i, natp i -> Vg f i <o r) -> n_sum f <=o r.
proof: Proof. move => axf ir ss. have sp: forall n, natp n -> n_sum_to_n f n <o r. apply: Nat_induction. move:Nat_order_wor => [wor sr]. by rewrite /n_sum_to_n /n_partial_sum (isum_p2 _ wor); case: ir. move => n nN hr; rewrite (nsum_p3 axf nN). apply: (indecomp_prop2 hr (ss _ nN) ir). by apply/ (nsum_p11c axf) => n /sp/proj1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)