proposition: Lemma ex_derive_sum_n : forall (f : nat -> K -> V) (n : nat) (x : K), (forall k, (k <= n)%nat -> ex_derive (f k) x) -> ex_derive (fun y => sum_n (fun k => f k y) n) x.
proof: Proof. intros f n x. elim: n => /= [ | n IH] Hf. eapply ex_derive_ext. intros t ; by rewrite sum_O. by apply (Hf O). eapply ex_derive_ext. intros t ; by rewrite sum_Sn. apply ex_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