proposition: Lemma increasing_interval_image : forall f lb ub x, increasing_interval lb ub f -> interval lb ub x -> interval (f lb) (f ub) (f x).
proof: Proof. intros f lb ub x Hf x_in ; assert (lb_le_ub : lb <= ub) by (eapply interval_inhabited ; eassumption) ; split ; apply Hf. apply interval_l ; assumption. assumption. apply x_in. assumption. apply interval_r ; assumption. apply x_in. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl MyRIneq MyR_dist Lra