proposition: Lemma derivable_pt_in_contravariant : forall D E f x, included D E -> derivable_pt_in E f x -> derivable_pt_in D f x.
proof: Proof. intros D E f x inc [l Hl] ; exists l ; apply derivable_pt_lim_in_contravariant with E ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Ranalysis_def Rfunction_facts MyRIneq MyR_dist Lra