proposition: Lemma Derive_opp : forall f x, Derive (fun x => - f x) x = - Derive f x.
proof: Proof. intros f x. unfold Derive, Lim. rewrite /Rbar_loc_seq. rewrite -Rbar.Rbar_opp_real. rewrite -Lim_seq_opp. apply f_equal, Lim_seq_ext => n. rewrite -Ropp_mult_distr_l_reverse. apply (f_equal (fun v => v / _)). ring. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv