proposition: Lemma continuous_abs {K : AbsRing} (x : K) : continuous abs x.
proof: Proof. apply filterlim_locally => /= eps. exists eps => /= y Hy. eapply Rle_lt_trans, Hy. wlog: x y Hy / (abs x <= abs y) => [Hw | Hxy]. case: (Rle_lt_dec (abs x) (abs y)) => Hxy. by apply Hw. rewrite abs_minus (abs_minus y). apply Hw, Rlt_le, Hxy. by apply ball_sym. rewrite {1}/abs /=. rewrite Rabs_pos_eq. apply Rle_minus_l. eapply Rle_trans, abs_triangle. apply Req_le, f_equal. by rewrite /minus -plus_assoc plus_opp_l plus_zero_r. by apply -> Rminus_le_0. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis