proposition: Lemma is_derive_Rabs (f : R -> R) (x df : R) : is_derive f x df -> f x <> 0 -> is_derive (fun x => Rabs (f x)) x (sign (f x) * df).
proof: Proof. intros Hf Hfx. evar_last. apply is_derive_comp, Hf. by apply filterdiff_Rabs. apply Rmult_comm. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis