proposition: Lemma nsum_p11c f a: nat_ord_seq f -> (forall n, natp n -> (n_sum_to_n f n) <=o a) -> n_sum f <=o a.
proof: Proof. move => ha hb. move: (proj32 (hb _ NS0)) => oa. rewrite (nsum_p11b ha). by apply: (ord_ub_sup oa) => i /funI_P [j jN ->]; apply: hb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)