proposition: Lemma nsum_p4 f n: nat_ord_seq f -> natp n -> n_sum_from_n f n = Vg f n +o n_sum_from_n f (csucc 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 (singleton n) (substrate Nat_order) by rewrite sr; apply: set1_sub. have rb: sub (Nat -s csucc n) (substrate Nat_order) by rewrite sr; apply: sub_setC. have rc i j: inc i (singleton n) -> inc j (Nat -s csucc n) -> glt Nat_order i j. move => /set1_P -> /setC_P [jN /(NleP nN)]; case: (NleT_el jN nN) => //. move => [la sa ] -. split => //. apply /Nat_order_leP; split => //; apply: (NS_le_nat sa nN). have rd: (singleton n \cup (Nat -s csucc n)) = (Nat -s n). rewrite (succ_of_nat nN) - setCC_l setU2_C setC1_K //;apply/setC_P. by split => //; apply: Nat_decent. by move: (isum_p4 wor fp ra rb rc); rewrite rd (isum_p3 wor fp ns). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)