proposition: Lemma monotonous_interval_image : forall f lb ub x, monotonous_interval lb ub f -> interval lb ub x -> interval (Rmin (f lb) (f ub)) (Rmax (f lb) (f ub)) (f x).
proof: Proof. intros f lb ub x [f_dec | f_inc] x_in ; assert (lbub : lb <= ub) by (eapply interval_inhabited, x_in). erewrite decreasing_in_Rmax_simpl, decreasing_in_Rmin_simpl ; try eassumption. apply decreasing_interval_image ; assumption. apply interval_l ; assumption. apply interval_r ; assumption. apply interval_l ; assumption. apply interval_r ; assumption. erewrite increasing_in_Rmax_simpl, increasing_in_Rmin_simpl ; try eassumption. apply increasing_interval_image ; assumption. apply interval_l ; assumption. apply interval_r ; assumption. apply interval_l ; assumption. apply interval_r ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl MyRIneq MyR_dist Lra