proposition: Lemma strictly_monotonous_interval_image : forall f lb ub x, strictly_monotonous_interval lb ub f -> open_interval lb ub x -> open_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 (left ; eapply open_interval_inhabited, x_in). erewrite decreasing_in_Rmax_simpl, decreasing_in_Rmin_simpl. apply strictly_decreasing_interval_image ; assumption. apply strictly_decreasing_in_decreasing_in ; eassumption. apply interval_l ; assumption. apply interval_r ; assumption. assumption. apply strictly_decreasing_in_decreasing_in ; eassumption. apply interval_l ; assumption. apply interval_r ; assumption. assumption. erewrite increasing_in_Rmax_simpl, increasing_in_Rmin_simpl. apply strictly_increasing_interval_image ; assumption. apply strictly_increasing_in_increasing_in ; eassumption. apply interval_l ; assumption. apply interval_r ; assumption. assumption. apply strictly_increasing_in_increasing_in ; eassumption. apply interval_l ; assumption. apply interval_r ; assumption. assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl MyRIneq MyR_dist Lra