proposition: Lemma limit_minus : forall (f g:R -> R) (D:R -> Prop) (l l' x0:R), limit1_in f D l x0 -> limit1_in g D l' x0 -> limit1_in (fun x:R => f x - g x) D (l - l') x0.
proof: Proof. intros; unfold Rminus; generalize (limit_Ropp g D l' x0 H0); intro; exact (limit_plus f (fun x:R => - g x) D l (- l') x0 H H1). Qed.
imports: Rbase Rfunctions Lra