proposition: Lemma pderive_increasing_closed_open : 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.
proof: Proof. move=> a b f pr ab H x y Hx Hy xy. case: (pderive_increasing_ax_closed_open pr ab) => H1 H2. case/Rle_lt_or_eq_dec : xy => xy. apply H2 => //. subst y. by apply Req_le. Qed.
imports: mathcomp(all_ssreflect) mathcomp(Rstruct) Reals Lra ssrR logb Reals_ext