proposition: Lemma derivable_pt_Ropp x : derivable_pt Ropp x.
proof: Proof. exists (-1) => eps Heps. exists (mkposreal _ Heps) => h /eqP Hh /= Hh'. rewrite (_ : (- (x + h) - - x) = - h); last by field. rewrite /Rdiv mulNR mulRV // (_ : -1 - -1 = 0); last by field. by rewrite Rabs_R0. Defined.
imports: mathcomp(all_ssreflect) mathcomp(Rstruct) Reals Lra ssrR logb Reals_ext