proposition: Lemma Derive_sum_n (f : nat -> R -> R) (n : nat) (x : R) : (forall k, (k <= n)%nat -> ex_derive (f k) x) -> Derive (fun y => sum_n (fun k => f k y) n) x = sum_n (fun k => Derive (f k) x) n.
proof: Proof. move => Hf. apply is_derive_unique. apply: is_derive_sum_n. move => k Hk. by apply Derive_correct, Hf. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv