proposition: Theorem D_in_imp : forall (f g:R -> R) (D D1:R -> Prop) (x:R), (forall x:R, D1 x -> D x) -> D_in f g D x -> D_in f g D1 x.
proof: Proof. intros f g D D1 x H; unfold D_in. intros H0; apply limit1_imp with (D := D_x D x); auto. intros x1 [H1 H2]; split; auto. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra