proposition: Lemma derivable_pt_lim_in_contravariant : forall D E f x l, included D E -> derivable_pt_lim_in E f x l -> derivable_pt_lim_in D f x l.
proof: Proof. intros D E f x l inc f_der ; apply limit1_in_contravariant with (D_x E x). apply D_x_covariant ; assumption. apply f_der. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Ranalysis_def Rfunction_facts MyRIneq MyR_dist Lra