proposition: Lemma limit_Ropp : forall (f:R -> R) (D:R -> Prop) (l x0:R), limit1_in f D l x0 -> limit1_in (fun x:R => - f x) D (- l) x0.
proof: Proof. unfold limit1_in; unfold limit_in; simpl; intros; elim (H eps H0); clear H; intros; elim H; clear H; intros; split with x; split; auto; intros; generalize (H1 x1 H2); clear H1; intro; unfold Rdist; unfold Rminus; rewrite (Ropp_involutive l); rewrite (Rplus_comm (- f x1) l); fold (l - f x1); fold (Rdist l (f x1)); rewrite Rdist_sym; assumption. Qed.
imports: Rbase Rfunctions Lra