proposition: Lemma pderive_increasing_ax_open_closed : forall (a b:R) (f:R -> R) (pr: pderivable f (fun x => a < x <= b)), a < b -> ((forall t:R, forall Ht :a < t <= b, 0 < derive_pt f t (pr t Ht)) -> forall x y:R, a < x <= b -> a < y <= b -> x < y -> f x < f y) /\ ((forall t:R, forall Ht : a < t <= b, 0 <= derive_pt f t (pr t Ht)) -> forall x y:R, a < x <= b -> a < y <= b -> x < y -> f x <= f y).
proof: Proof. intros a b f pr H; split; intros H0 x y H1 H2 H3. - rewrite -subR_gt0. set pr' := pderivable_restrict_left pr (proj1 H1) (proj2 H2) H3. have H0' : forall t (Ht : x <= t <= y), 0 < derive_pt f t (pr' t Ht). move=> z /= [Hz0 Hz1]. by apply H0. case: (MVT_cor1_pderivable pr' H3); intros x0 [x1 [H7 H8]]. rewrite H7. apply mulR_gt0; [by apply H0' | lra]. - set pr' := pderivable_restrict_left pr (proj1 H1) (proj2 H2) H3. have H0' : forall t (Ht : x <= t <= y), 0 <= derive_pt f t (pr' t Ht). move=> z /= [Hz0 Hz1]. by apply H0. case: (MVT_cor1_pderivable pr' H3); intros x0 [x1 [H7 H8]]. rewrite -(add0R (f x)) -leR_subr_addr H7; apply mulR_ge0 => //; lra. Qed.
imports: mathcomp(all_ssreflect) mathcomp(Rstruct) Reals Lra ssrR logb Reals_ext