proposition: Lemma limit_free : forall (f:R -> R) (D:R -> Prop) (x x0:R), limit1_in (fun h:R => f x) D (f x) x0.
proof: Proof. unfold limit1_in; unfold limit_in; simpl; intros; split with eps; split; auto; intros; elim (Rdist_refl (f x) (f x)); intros a b; rewrite (b (eq_refl (f x))); unfold Rgt in H; assumption. Qed.
imports: Rbase Rfunctions Lra