proposition: Lemma Dopp : forall (D:R -> Prop) (f df:R -> R) (x0:R), D_in f df D x0 -> D_in (fun x:R => - f x) (fun x:R => - df x) D x0.
proof: Proof. intros; generalize (Dmult_const D f df x0 (-1) H); unfold D_in; unfold limit1_in; unfold limit_in; intros; generalize (H0 eps H1); clear H0; intro; elim H0; clear H0; intros; elim H0; clear H0; simpl; intros; split with x; split; auto. intros; generalize (H2 x1 H3); clear H2; intro. replace (- f x1 - - f x0) with (-1 * f x1 - -1 * f x0) by ring. replace (- df x0) with (-1 * df x0) by ring. exact H2. Qed.
imports: Rbase Rfunctions Rlimit Lra Lia