proposition: Lemma filterdiff_iter_plus_fct {I} {F} {FF : Filter F} (l : list I) (f : I -> U -> V) df (x : U) : (forall (j : I), List.In j l -> filterdiff (f j) F (df j)) -> filterdiff (fun y => iter plus zero l (fun j => f j y)) F (fun x => iter plus zero l (fun j => df j x)).
proof: Proof. intros Hf. induction l ; simpl in * |- *. apply filterdiff_const. apply filterdiff_plus_fct. apply Hf. by left. apply IHl ; intros. apply Hf. by right. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv