proposition: Lemma nsum_p3 f n: nat_ord_seq f -> natp n -> n_sum_to_n f (csucc n) = n_sum_to_n f n +o Vg f n.
proof: Proof. move => /nsum_p0 fp nN. move:Nat_order_wor => [wor sr]. have ns: inc n (substrate Nat_order) by ue. have ra: sub n (substrate Nat_order) by rewrite sr; apply: NS_inc_nat. have rb: sub (singleton n) (substrate Nat_order). by rewrite sr; apply: set1_sub. have rc i j: inc i n -> inc j (singleton n) -> glt Nat_order i j. move =>/(NltP nN) [sa sb] /set1_P ->; split => //. apply /Nat_order_leP; split => //; apply: (NS_le_nat sa nN). move: (isum_p4 wor fp ra rb rc). by rewrite (isum_p3 wor fp ns) (succ_of_nat nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)