proposition: Lemma Dx : forall (D:R -> Prop) (x0:R), D_in (fun x:R => x) (fun x:R => 1) D x0.
proof: Proof. unfold D_in; unfold Rdiv; intros; unfold limit1_in; unfold limit_in; intros; simpl; split with eps; split; auto. intros; elim H0; clear H0; intros; unfold D_x in H0; elim H0; intros; rewrite (Rinv_r (x - x0) (Rminus_eq_contra x x0 (sym_not_eq H3))); unfold Rdist; rewrite (Rminus_diag_eq 1 1 (refl_equal 1)); unfold Rabs; case (Rcase_abs 0) as [Hlt|Hge]. - absurd (0 < 0); auto. red in |- *; intro; apply (Rlt_irrefl 0 Hlt). - unfold Rgt in H; assumption. Qed.
imports: Rbase Rfunctions Rlimit Lra Lia