proposition: Lemma pr_nu_var2_interv : forall (f g : R -> R) (lb ub x : R) (pr1 : derivable_pt f x) (pr2 : derivable_pt g x), open_interval lb ub x -> (forall h : R, lb < h < ub -> f h = g h) -> derive_pt f x pr1 = derive_pt g x pr2.
proof: Proof. intros f g lb ub x Prf Prg x_encad local_eq. assert (forall x l, lb < x < ub -> (derivable_pt_abs f x l <-> derivable_pt_abs g x l)). intros a l a_encad. unfold derivable_pt_abs, derivable_pt_lim. split. intros Hyp eps eps_pos. elim (Hyp eps eps_pos) ; intros delta Hyp2. assert (Pos_cond : Rmin delta (Rmin (ub - a) (a - lb)) > 0). clear-a lb ub a_encad delta. apply Rmin_pos_lt ; [exact (delta.(cond_pos)) | apply Rmin_pos_lt ] ; apply Rlt_Rminus ; intuition. exists (mkposreal (Rmin delta (Rmin (ub - a) (a - lb))) Pos_cond). intros h h_neq h_encad. replace (g (a + h) - g a) with (f (a + h) - f a). apply Hyp2 ; intuition. apply Rlt_le_trans with (r2:=Rmin delta (Rmin (ub - a) (a - lb))). assumption. apply Rmin_l. assert (local_eq2 : forall h : R, lb < h < ub -> - f h = - g h). intros ; apply Ropp_eq_compat ; intuition. rewrite local_eq ; unfold Rminus. rewrite local_eq2. reflexivity. assumption. assert (Sublemma2 : forall x y, Rabs x < Rabs y -> y > 0 -> x < y). intros m n Hyp_abs y_pos. apply Rlt_le_trans with (r2:=Rabs n). apply Rle_lt_trans with (r2:=Rabs m) ; [ | assumption] ; apply RRle_abs. apply Req_le ; apply Rabs_right ; apply Rgt_ge ; assumption. split. assert (Sublemma : forall x y z, -z < y - x -> x < y + z). intros ; lra. apply Sublemma. apply Sublemma2. rewrite Rabs_Ropp. apply Rlt_le_trans with (r2:=a-lb) ; [| apply RRle_abs] ; apply Rlt_le_trans with (r2:=Rmin (ub - a) (a - lb)) ; [| apply Rmin_r] ; apply Rlt_le_trans with (r2:=Rmin delta (Rmin (ub - a) (a - lb))) ; [| apply Rmin_r] ; assumption. apply Rlt_le_trans with (r2:=Rmin (ub - a) (a - lb)) ; [| apply Rmin_r] ; apply Rlt_le_trans with (r2:=Rmin delta (Rmin (ub - a) (a - lb))) ; [| apply Rmin_r] ; assumption. assert (Sublemma : forall x y z, y < z - x -> x + y < z). intros ; lra. apply Sublemma. apply Sublemma2. apply Rlt_le_trans with (r2:=ub-a) ; [| apply RRle_abs] ; apply Rlt_le_trans with (r2:=Rmin (ub - a) (a - lb)) ; [| apply Rmin_l] ; apply Rlt_le_trans with (r2:=Rmin delta (Rmin (ub - a) (a - lb))) ; [| apply Rmin_r] ; assumption. apply Rlt_le_trans with (r2:=Rmin (ub - a) (a - lb)) ; [| apply Rmin_l] ; apply Rlt_le_trans with (r2:=Rmin delta (Rmin (ub - a) (a - lb))) ; [| apply Rmin_r] ; assumption. intros Hyp eps eps_pos. elim (Hyp eps eps_pos) ; intros delta Hyp2. assert (Pos_cond : Rmin delta (Rmin (ub - a) (a - lb)) > 0). clear-a lb ub a_encad delta. apply Rmin_pos_lt ; [exact (delta.(cond_pos)) | apply Rmin_pos_lt ] ; apply Rlt_Rminus ; intuition. exists (mkposreal (Rmin delta (Rmin (ub - a) (a - lb))) Pos_cond). intros h h_neq h_encad. replace (f (a + h) - f a) with (g (a + h) - g a). apply Hyp2 ; intuition. apply Rlt_le_trans with (r2:=Rmin delta (Rmin (ub - a) (a - lb))). assumption. apply Rmin_l. assert (local_eq2 : forall h : R, lb < h < ub -> - f h = - g h). intros ; apply Ropp_eq_compat ; intuition. rewrite local_eq ; unfold Rminus. rewrite local_eq2. reflexivity. assumption. assert (Sublemma2 : forall x y, Rabs x < Rabs y -> y > 0 -> x < y). intros m n Hyp_abs y_pos. apply Rlt_le_trans with (r2:=Rabs n). apply Rle_lt_trans with (r2:=Rabs m) ; [ | assumption] ; apply RRle_abs. apply Req_le ; apply Rabs_right ; apply Rgt_ge ; assumption. split. assert (Sublemma : forall x y z, -z < y - x -> x < y + z). intros ; lra. apply Sublemma. apply Sublemma2. rewrite Rabs_Ropp. apply Rlt_le_trans with (r2:=a-lb) ; [| apply RRle_abs] ; apply Rlt_le_trans with (r2:=Rmin (ub - a) (a - lb)) ; [| apply Rmin_r] ; apply Rlt_le_trans with (r2:=Rmin delta (Rmin (ub - a) (a - lb))) ; [| apply Rmin_r] ; assumption. apply Rlt_le_trans with (r2:=Rmin (ub - a) (a - lb)) ; [| apply Rmin_r] ; apply Rlt_le_trans with (r2:=Rmin delta (Rmin (ub - a) (a - lb))) ; [| apply Rmin_r] ; assumption. assert (Sublemma : forall x y z, y < z - x -> x + y < z). intros ; lra. apply Sublemma. apply Sublemma2. apply Rlt_le_trans with (r2:=ub-a) ; [| apply RRle_abs] ; apply Rlt_le_trans with (r2:=Rmin (ub - a) (a - lb)) ; [| apply Rmin_l] ; apply Rlt_le_trans with (r2:=Rmin delta (Rmin (ub - a) (a - lb))) ; [| apply Rmin_r] ; assumption. apply Rlt_le_trans with (r2:=Rmin (ub - a) (a - lb)) ; [| apply Rmin_l] ; apply Rlt_le_trans with (r2:=Rmin delta (Rmin (ub - a) (a - lb))) ; [| apply Rmin_r] ; assumption. unfold derivable_pt in Prf. unfold derivable_pt in Prg. elim Prf; intros. elim Prg; intros. assert (Temp := p); rewrite H in Temp. unfold derivable_pt_abs in p. unfold derivable_pt_abs in p0. simpl in |- *. apply (uniqueness_limite g x x0 x1 Temp p0). assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Ranalysis_def Rfunction_facts MyRIneq MyR_dist Lra