proposition: Lemma derive_sincreasing_interv a b (f:R -> R) (pr: pderivable f (fun x => a < x < b)) (prc : forall x (Hx : a <= x <= b), continuity_pt f x) : a < b -> ((forall t:R, forall (prt : derivable_pt f t), a < t < b -> 0 < derive_pt f t prt) -> forall x y:R, a <= x <= b -> a <= y <= b -> x < y -> f x < f y).
proof: Proof. intros H H0 x y H1 H2 H3. rewrite -subR_gt0. have prd' : pderivable f (fun z => x < z < y). move=> z /= [Hz1 Hz2] ; apply pr. split. - apply (@leR_ltR_trans x) => //; by apply H1. - apply (@ltR_leR_trans y) => //; by apply H2. have H0' : forall t (Ht : x < t < y), 0 < derive_pt f t (prd' t Ht). move=> z /= [Hz0 Hz1]. apply H0. split. - apply (@leR_ltR_trans x) => //; by apply H1. - apply (@ltR_leR_trans y) => //; by apply H2. have prcx : continuity_pt f x by apply prc; split; apply H1. have prcy : continuity_pt f y by apply prc; split; apply H2. have aux : a < b. apply (@leR_ltR_trans x) ; first by apply H1. apply (@ltR_leR_trans y) => //; by apply H2. case: (MVT_cor1_pderivable_open_continuity prd' prcx prcy H3); intros x0 [x1 [H7 H8]]. rewrite H7. apply mulR_gt0; first by apply H0'. by rewrite subR_gt0. Qed.
imports: mathcomp(all_ssreflect) mathcomp(Rstruct) Reals Lra ssrR logb Reals_ext