proposition: Theorem D_in_ext : forall (f g h:R -> R) (D:R -> Prop) (x:R), f x = g x -> D_in h f D x -> D_in h g D x.
proof: Proof. intros f g h D x H; unfold D_in. rewrite H; auto. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra