proposition: Lemma strictly_decreasing_strictly_increasing_interval2 : forall f lb ub, strictly_decreasing_interval lb ub f -> strictly_increasing_interval (-ub) (-lb) (fun x => f(-x)).
proof: Proof. intros f c r f_decr ; intros x y x_in_B y_in_B x_lt_y. apply f_decr ; unfold interval in * ; try split ; intuition ; lra. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl MyRIneq MyR_dist Lra