proposition: Theorem Xderive_pt_abs : forall f f' x, Xderive_pt f x f' -> Xderive_pt (fun x => Xabs (f x)) x (match Xcmp (f x) (Xreal 0) with Xlt => Xneg f' | Xgt => f' | _ => Xnan end).
proof: Proof. intros f f' x Hf. xtotal. revert X. now case Xcmp. revert X. now case Xcmp. simpl Xcmp in X0. destruct (Rcompare_spec r1 0) ; try easy. intro v. apply derivable_pt_lim_eq_locally with (fun x => Ropp (proj_fun v f x)). apply locally_true_imp with (2 := derivable_imp_defined_lt _ _ _ _ _ X H Hf). intros x (w, (Hw1, Hw2)). unfold proj_fun. rewrite Hw2. now rewrite Rabs_left. inversion X0. now apply derivable_pt_lim_opp. intro v. apply derivable_pt_lim_eq_locally with (proj_fun v f). apply locally_true_imp with (2 := derivable_imp_defined_gt _ _ _ _ _ X H Hf). intros x (w, (Hw1, Hw2)). unfold proj_fun. rewrite Hw2. rewrite Rabs_right. apply refl_equal. apply Rle_ge. now apply Rlt_le. inversion X0. now rewrite <- H1. Qed.
imports: Coq(Reals) Flocq(Raux) Stdlib Xreal