proposition: Lemma lim_x : forall (D:R -> Prop) (x0:R), limit1_in (fun x:R => x) D x0 x0.
proof: Proof. unfold limit1_in; unfold limit_in; simpl; intros; split with eps; split; auto; intros; elim H0; intros; auto. Qed.
imports: Rbase Rfunctions Lra