proposition: Lemma is_derive_sum_n : forall (f : nat -> K -> V) (n : nat) (x : K) (d : nat -> V), (forall k, (k <= n)%nat -> is_derive (f k) x (d k)) -> is_derive (fun y => sum_n (fun k => f k y) n) x (sum_n d n).
proof: Proof. intros f n x d. elim: n => /= [ | n IH] Hf. rewrite sum_O. eapply is_derive_ext, (Hf O) => //. intros t ; by rewrite sum_O. eapply is_derive_ext. intros t ; apply sym_eq, sum_Sn. rewrite sum_Sn. apply is_derive_plus. apply IH => k Hk. by apply Hf, Nat.le_trans with (1 := Hk), Nat.le_succ_diag_r. by apply Hf. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv