proposition: Lemma derive_increasing_interv : forall (a b : R) (f : R -> R), a < b -> forall (pr:forall x, a < x < b -> derivable_pt f x), (forall t:R, forall (t_encad : a < t < b), 0 < derive_pt f t (pr t t_encad)) -> forall x y:R, a < x < b -> a < y < b -> x < y -> f x < f y.
proof: Proof. intros a b f a_lt_b pr Df_gt_0 x y x_encad y_encad x_lt_y. assert (derivable_id_interv : forall c : R, x < c < y -> derivable_pt id c). { intros ; apply derivable_pt_id. } assert (derivable_f_interv : forall c : R, x < c < y -> derivable_pt f c). { intros c c_encad. apply pr. split. { apply Rlt_trans with (r2:=x) ; [exact (proj1 x_encad) | exact (proj1 c_encad)]. } apply Rlt_trans with (r2:=y) ; [exact (proj2 c_encad) | exact (proj2 y_encad)]. } assert (f_cont_interv : forall c : R, x <= c <= y -> continuity_pt f c). { intros c c_encad; apply derivable_continuous_pt ; apply pr. split. { apply Rlt_le_trans with (r2:=x) ; [exact (proj1 x_encad) | exact (proj1 c_encad)]. } apply Rle_lt_trans with (r2:=y) ; [ exact (proj2 c_encad) | exact (proj2 y_encad)]. } assert (id_cont_interv : forall c : R, x <= c <= y -> continuity_pt id c). { intros ; apply derivable_continuous_pt ; apply derivable_pt_id. } elim (MVT f id x y derivable_f_interv derivable_id_interv x_lt_y f_cont_interv id_cont_interv). intros c Temp ; elim Temp ; clear Temp ; intros Pr eq. replace (id y - id x) with (y - x) in eq by intuition. replace (derive_pt id c (derivable_id_interv c Pr)) with 1 in eq. 2:{ symmetry ; rewrite derive_pt_eq ; apply derivable_pt_lim_id. } apply Rminus_gt. rewrite Rmult_1_r in eq. rewrite <- eq. apply Rmult_gt_0_compat. { apply Rgt_minus ; assumption. } assert (c_encad2 : a <= c < b). { split. { apply Rlt_le ; apply Rlt_trans with (r2:=x) ; [exact (proj1 x_encad) | exact (proj1 Pr)]. } apply Rle_lt_trans with (r2:=y) ; [apply Rlt_le ; exact (proj2 Pr) | exact (proj2 y_encad)]. } assert (c_encad : a < c < b). { split. { apply Rlt_trans with (r2:=x) ; [exact (proj1 x_encad) | exact (proj1 Pr)]. } apply Rle_lt_trans with (r2:=y) ; [apply Rlt_le ; exact (proj2 Pr) | exact (proj2 y_encad)]. } rewrite (pr_nu f c (derivable_f_interv c Pr) (pr c c_encad)). apply (Df_gt_0 c c_encad). Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia