proposition: Lemma increasing_in_contravariant : forall D E f, included D E -> increasing_in E f -> increasing_in D f.
proof: Proof. intros D E f inc f_inc x y x_in y_in Hxy ; apply f_inc ; try apply inc ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Ranalysis_def Rfunction_facts MyRIneq MyR_dist Lra