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