proposition: Lemma limit1_in_contravariant : forall D E f x l, included D E -> limit1_in f E x l -> limit1_in f D x l.
proof: Proof. intros D E f x l inc Hfxl eps eps_pos ; destruct (Hfxl _ eps_pos) as [alp [alp_pos Halp]] ; exists alp ; split. assumption. intros y [Dy y_bd] ; apply Halp ; split ; [apply inc |] ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Ranalysis_def Rfunction_facts MyRIneq MyR_dist Lra