proposition: Lemma derive_pt_comp_Ropp : forall a b f x (Df : forall x, open_interval a b x -> derivable_pt f x) (Df' : forall x, open_interval (-b) (-a) x -> derivable_pt (fun x0 => f (- x0)) x) (H1 : open_interval (-b) (-a) x) (H2 : open_interval a b (-x)), - derive_pt f (- x) (Df (- x) H2) = derive_pt (fun x0 : R => f (- x0)) x (Df' x H1).
proof: Proof. intros. assert (derivable_pt (comp f (fun x=> Ropp x)) x). reg. apply derivable_pt_opp. reg. apply Df. apply H2. assert (Heq : forall x, (fun x0 => f (-x0)) x = (comp f (fun x => Ropp x)) x). intros. reflexivity. rewrite (derive_pt_ext (fun x0 => f (-x0)) (comp f (fun x => Ropp x)) Heq x (Df' (x) H1) H). assert (derivable_pt (fun x => (-x)) x). reg. assert (derivable_pt f ((fun x => -x) x)). apply Df. apply H2. pose (p := derivable_pt_comp (fun x => (-x)) f x H0 H3). rewrite (pr_nu_var _ _ _ H p). unfold p. rewrite derive_pt_comp. replace (derive_pt (fun x0 : R => (- x0)%R) x H0) with (-(1%R)). ring_simplify. apply Ropp_eq_compat. apply pr_nu. rewrite <- derive_pt_id with x. rewrite <- derive_pt_opp. unfold id. apply pr_nu. reflexivity. Qed.
imports: Reals Lra Rfunction_classes_def Cauchy_lipschitz Rextensionality