proposition: Lemma nsum_p0 f: nat_ord_seq f -> [/\ fgraph f, domain f = substrate Nat_order & allf f ordinalp].
proof: Proof. move:Nat_order_wor => [wor sr] [ha hb hc]. split => //; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)