proposition: Lemma nsum_p1 f: nat_ord_seq f -> n_sum f = n_partial_sum f Nat.
proof: Proof. move:Nat_order_wor => [[or _] sr] [ha hb hc]; rewrite /n_sum /n_partial_sum /ipartial_sum - {1} sr (iorder_substrate or). by rewrite - hb restr_to_domain. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)