proposition: Lemma derivable_in_contravariant : forall D E f, included D E -> derivable_in E f -> derivable_in D f.
proof: Proof. intros D E f inc f_der x Dx ; apply derivable_pt_in_contravariant with E. assumption. apply f_der, inc ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Ranalysis_def Rfunction_facts MyRIneq MyR_dist Lra