proposition: Lemma filterdiff_Rabs (x : R) : x <> 0 -> filterdiff Rabs (locally x) (fun y : R => scal y (sign x)).
proof: Proof. rewrite -/(is_derive Rabs x (sign x)). move => Hx0. case: (Rle_lt_dec 0 x) => Hx. case: Hx => //= Hx. rewrite sign_eq_1 //. eapply is_derive_ext_loc. apply locally_interval with 0 p_infty. by []. by []. move => /= y Hy _. rewrite Rabs_pos_eq //. by apply Rlt_le. by apply @is_derive_id. by apply sym_eq in Hx. rewrite sign_eq_m1 //. eapply is_derive_ext_loc. apply locally_interval with m_infty 0. by []. by []. move => /= y _ Hy. rewrite -Rabs_Ropp Rabs_pos_eq //. rewrite -Ropp_0 ; by apply Rlt_le, Ropp_lt_contravar. apply @is_derive_opp. by apply @is_derive_id. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis