proposition: Lemma Rcontinuity_abs : continuity Rabs.
proof: Proof. unfold continuity; intro. case (Req_dec x 0); intro. - unfold continuity_pt; unfold continue_in; unfold limit1_in; unfold limit_in; simpl; unfold Rdist; intros; exists eps; split. + apply H0. + intros; rewrite H; rewrite Rabs_R0; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; rewrite Rabs_Rabsolu; elim H1; intros; rewrite H in H3; unfold Rminus in H3; rewrite Ropp_0 in H3; rewrite Rplus_0_r in H3; apply H3. - apply derivable_continuous_pt; apply (Rderivable_pt_abs x H). Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Ranalysis3 Exp_prop MVT Lra Lia