fact: Definition Dpow (n : nat) := match n with | O => fun _ => 0 | S m => fun x => (INR (S m)) * pow x m end.
imports: Rbase Ranalysis Rfunctions Rfunction_def MyRIneq Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_facts