proposition: Lemma strictly_decreasing_in_opp_rev : forall D f, strictly_decreasing_in D (- f)%F -> strictly_increasing_in D f.
proof: Proof. intros D f Hf x y Dx Dy Hxy ; unfold opp_fct ; apply Ropp_lt_cancel, Hf ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl MyRIneq MyR_dist Lra