proposition: Lemma nsum_p2 f n: nat_ord_seq f -> natp n -> n_sum f = n_sum_to_n f n +o n_sum_from_n f n.
proof: Proof. move:Nat_order_wor => [wor sr] fp nN; rewrite (nsum_p1 fp). move /nsum_p0: fp => fp. have ra : sub n (substrate Nat_order) by rewrite sr;apply: NS_inc_nat. have rb: sub (Nat -s n) (substrate Nat_order) by rewrite sr; apply: sub_setC. have rc i j: inc i n -> inc j (Nat -s n) -> glt Nat_order i j. move => /(NltP nN) iN /setC_P [jN /(NltP nN) h ]. have: i <c j by case: (NleT_el nN jN) => // lnj ; apply:(clt_leT iN lnj). move => [lij nij]; split => //; apply /Nat_order_leP; split => //. apply: (NS_le_nat lij jN). symmetry; move:(isum_p4 wor fp ra rb rc). by rewrite setU2_C; move/setCU_K: ra; rewrite sr => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)