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