proposition: Lemma is_derive_n_iter_plus {I : Type} (l : list I) (f : I -> R -> R) (n: nat) (x : R) : locally x (fun y => forall (j : I) (k : nat), List.In j l -> (k <= n)%nat -> ex_derive_n (f j) k y) -> is_derive_n (fun y => iter Rplus 0 l (fun j => f j y)) n x (iter Rplus 0 l (fun j => Derive_n (f j) n x)).
proof: Proof. intros H. elim: n {-2}n x (Nat.le_refl n) H => [ | n IH] m x Hn Hx. now replace m with O by intuition. apply le_lt_eq_dec in Hn ; case: Hn => Hn. apply IH => //. by apply Nat.lt_succ_r. rewrite Hn in Hx |- * => {m Hn} /=. eapply is_derive_ext_loc. eapply filter_imp. intros y Hy. apply sym_equal, is_derive_n_unique. apply IH. by apply Nat.le_refl. apply Hy. apply locally_locally. move: Hx ; apply filter_imp. move => y Hy j k Hj Hk. apply Hy => //. now eapply Nat.le_trans, Nat.le_succ_diag_r. eapply filterdiff_ext_lin. apply @filterdiff_iter_plus_fct => //. apply locally_filter. intros. apply Derive_correct. apply ((locally_singleton _ _ Hx) j (S n) H (Nat.le_refl _)). simpl => y. clear ; elim: l => /= [ | h l IH]. by rewrite scal_zero_r. by rewrite IH scal_distr_l. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv