proposition: Lemma OS_nsum f E: nat_ord_seq f -> sub E Nat -> ordinalp (n_partial_sum f E).
proof: Proof. move:Nat_order_wor => [wor sr] /nsum_p0 fp En. have sE: sub E (substrate Nat_order) by ue. exact (isum_p1 wor fp sE). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)