proposition: Lemma D_x_covariant : forall D E x, included D E -> included (D_x D x) (D_x E x).
proof: Proof. intros D E x inc y [y_neq y_in] ; split ; [apply inc |] ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Ranalysis_def Rfunction_facts MyRIneq MyR_dist Lra