fact: Definition derive_Rball c r f (pr : derivable_Rball c r f) x := match in_Rball_dec c r x with | left P => derive_pt_in (Rball c r) f x (pr x P) | right P => 0 end.
imports: Rbase Rpower Lra Ranalysis1 Ranalysis2 Rfunctions MyRIneq Rtopology Rinterval Rfunction_facts