proposition: Lemma increasing_in_minus : forall D f g, increasing_in D f -> decreasing_in D g -> increasing_in D (f - g)%F.
proof: Proof. intros D f g Hf Hg x y Dx Dy Hxy ; unfold plus_fct ; apply Rplus_le_compat ; [apply Hf | apply Ropp_le_contravar, Hg] ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl MyRIneq MyR_dist Lra