proposition: Lemma is_derive_opp : forall (f : K -> V) (x : K) (l : V), is_derive f x l -> is_derive (fun x => opp (f x)) x (opp l).
proof: Proof. intros f x l Df. apply filterdiff_ext_lin with (fun t : K => opp (scal t l)). apply filterdiff_comp' with (1 := Df). apply filterdiff_opp. intros y. apply sym_eq. apply: scal_opp_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv