proposition: Lemma nsum_p10g f: nat_ord_seq f -> n_sum f = (n_partial_sum f (n_sum_small_idx f)) +o (n_sum_rem f).
proof: Proof. move => ha. rewrite /n_sum_small_idx/n_sum_rem; Ytac h; Ytac0. by apply: nsum_p10f. by apply: nsum_p10e. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)