proposition: Lemma Rderivable_pt_abs : forall x:R, x <> 0 -> derivable_pt Rabs x.
proof: Proof. intros. destruct (total_order_T x 0) as [[Hlt|Heq]|Hgt]. - unfold derivable_pt; exists (-1). apply (Rabs_derive_2 x Hlt). - elim H; exact Heq. - unfold derivable_pt; exists 1. apply (Rabs_derive_1 x Hgt). Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Ranalysis3 Exp_prop MVT Lra Lia