proposition: Lemma pderive_increasing (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 < if t == b then 1 else 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. move=> H H0 x y H1 H2 H3. apply/subR_gt0. set pr' := pderivable_restrict_left pr (proj1 H1) (proj2 H2) H3. have H0' : forall t (Ht : x <= t <= y), 0 < if t == y then 1 else derive_pt f t (pr' t Ht). move=> z /= [Hz0 Hz1]. case/orP : (orbN (z == y)) => Hcase. - rewrite Hcase ; lra. - move/negbTE in Hcase ; rewrite Hcase. have Hz : a < z <= b. split. - apply: (ltR_leR_trans _ Hz0); by apply H1. - apply: (leR_trans Hz1); by apply H2. move: (H0 z) => H02. have Hz2 : ~~ (z == b). apply/ltR_eqF. clear Hz0 H1 H3 pr' H H0 x. move/eqP in Hcase. apply (@ltR_leR_trans y). - case (total_order_T z y) ; first case ; move=> Hzy. - exact Hzy. - contradict Hcase ; exact Hzy. - lra. - by apply H2. move/negbTE in Hz2. rewrite Hz2 in H02. by apply H02. case: (MVT_cor1_pderivable pr' H3); intros x0 [x1 [H7 H8]]. rewrite H7. apply mulR_gt0; last lra. have Hx0 : ~~ (x0 == y) by rewrite ltR_eqF //; case: H8. move/negbTE in Hx0. by move: (H0' x0); rewrite Hx0; exact. Qed.
imports: mathcomp(all_ssreflect) mathcomp(Rstruct) Reals Lra ssrR logb Reals_ext