proposition: Lemma derive_open_interval_pos_strictly_increasing_open_interval : forall f lb ub (pr : derivable_open_interval lb ub f), (forall x, open_interval lb ub x -> 0 < derive_open_interval lb ub f pr x) -> strictly_increasing_open_interval lb ub f.
proof: Proof. intros f lb ub pr Df_pos x y x_in y_in Hxy. assert (pr1 : forall c : R, open_interval x y c -> derivable_pt f c). intros ; eapply derivable_open_interval_pt ; [eapply pr |]. eapply open_interval_restriction ; try eassumption ; apply open_interval_interval ; eassumption. assert (pr2 : forall c : R, open_interval x y c -> derivable_pt id c). intros ; apply derivable_id. destruct (MVT f id x y pr1 pr2 Hxy) as [c [c_in Hc]]. intros ; eapply derivable_continuous_pt, derivable_open_interval_pt ; [eapply pr | apply interval_open_restriction with x y ; assumption]. intros ; reg. unfold id in Hc ; fold id in Hc ; replace (derive_pt id c (pr2 c c_in)) with 1 in Hc ; [rewrite Rmult_1_r in Hc |]. apply Rminus_gt ; rewrite <- Hc ; apply Rmult_lt_0_compat ; [lra |]. erewrite <- derive_open_interval_derive_pt ; [eapply Df_pos |] ; eapply open_interval_restriction ; try (eapply open_interval_interval || apply c_in) ; eassumption. symmetry ; apply derive_pt_id. Qed.
imports: Rbase Rpower Ranalysis Lra Rfunctions Rfunction_def Rextensionality MyRIneq MyR_dist Rtopology Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity