proposition: Lemma osum_f1r p n: natp n -> ord_below p (csucc n) -> osumf p (csucc n) = osumf (fun i => p (csucc i)) n +o p \0c.
proof: Proof. move => nN ax. have op0: ordinalp (p \0c) by apply: ax; apply: succ_positive. move: ax;rewrite (Nsucc_rw nN) csumC => ax. rewrite (osum_fA NS1 nN ax) (osum_f1 op0); apply: f_equal2;last exact. by apply: (osumf_exten nN) => i lin; rewrite (Nsucc_rw (NS_lt_nat lin nN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)