proposition: Lemma nsum_p11b f: nat_ord_seq f -> n_sum f = \osup (fun_image Nat (n_sum_to_n f)).
proof: Proof. move => ha. move:Nat_order_wor => [wor sr]. move: (nsum_p0 ha) => ax. case:(isum_p7b wor ax). move => [n []]; rewrite sr => nN h. move:(h _ (NS_succ nN)) => /Nat_order_leP [ _ _ /cleNgt]; case; exact: cltS. rewrite (nsum_p1 ha) sr /n_partial_sum => ->. rewrite /n_sum_to_n /n_partial_sum. apply: f_equal;apply: funI_exten => i iN; apply:f_equal. set_extens t. by move => /Zo_P[tN [/Nat_order_leP [_ _ qa] qb] ]; apply/(NltP iN). move/(NltP iN) =>[qa qb]; move: (NS_le_nat qa iN) => tN. by apply: (Zo_i tN); split => //;apply/Nat_order_leP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)