[STATEMENT]
lemma isFDERIV_imp_isFDERIV_FDERIV_n:
  assumes "length fas = length ds"
  shows "isFDERIV N xs fas vs \<Longrightarrow> isFDERIV N xs ds vs \<Longrightarrow>
    isFDERIV N xs (FDERIV_n_floatariths fas xs ds n) vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isFDERIV N xs fas vs; isFDERIV N xs ds vs\<rbrakk> \<Longrightarrow> isFDERIV N xs (FDERIV_n_floatariths fas xs ds n) vs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length fas = length ds

goal (1 subgoal):
 1. \<lbrakk>isFDERIV N xs fas vs; isFDERIV N xs ds vs\<rbrakk> \<Longrightarrow> isFDERIV N xs (FDERIV_n_floatariths fas xs ds n) vs
[PROOF STEP]
by (induction n) (auto intro!: isDERIV_FDERIV_floatariths)