proposition: Lemma prod_SO_split : forall (An:nat -> R) (n k:nat), (k < n)%nat -> prod_f_R0 An n = prod_f_R0 An k * prod_f_R0 (fun l:nat => An (k +1+l)%nat) (n - k -1).
proof: Proof. intros; induction n as [| n Hrecn]. - absurd (k < 0)%nat; lia. - cut (k = n \/ (k < n)%nat);[intro; elim H0; intro|lia]. + replace (S n - k - 1)%nat with O; [rewrite H1; simpl|lia]. replace (n+1+0)%nat with (S n); ring. + replace (S n - k-1)%nat with (S (n - k-1));[idtac|lia]. simpl; replace (k + S (n - k))%nat with (S n). * replace (k + 1 + S (n - k - 1))%nat with (S n). -- rewrite Hrecn; [ ring | assumption ]. -- lia. * lia. Qed.
imports: Compare Rbase Rfunctions Rseries PartSum Binomial Lia