proposition: Lemma osum_fA n m f: natp n -> natp m -> ord_below f (n +c m) -> osumf f (n +c m) = (osumf (fun z => f (z +c n)) m) +o (osumf f n).
proof: Proof. move => nN mN; move: m mN n nN; apply: Nat_induction. move => n nN; rewrite (Nsum0r nN) (osum_f0) => fo. rewrite osum0l //; apply:OS_osumf => //. move => m mN Hrec n nN. have nmN:= NS_sum nN mN. rewrite (csum_nS _ mN) (osum_fS _ nmN). move => /(true_below_rec nmN) [pa pb]. have pc: ordinalp (osumf (fun z => f (z +c n)) m). apply: OS_osumf => // k km; apply: pa. by move: (csum_Mlteq nN km); rewrite csumC (csumC m). have pd: ordinalp (osumf f n). apply: OS_osumf => // k km;apply: pa. exact:(clt_leT km (Nsum_M0le m nN)). by rewrite Hrec // (osumA pb pc pd) (osum_fS _ mN) csumC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)