# Library Coqtail.Reals.Ranalysis.Ranalysis_usual

Require Import Rbase Ranalysis Rfunctions Rfunction_def.
Require Import MyRIneq.
Require Import Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_facts.

Local Open Scope R_scope.

# Identity

Lemma derivable_pt_lim_in_id: D x,
derivable_pt_lim_in D id x 1.
Proof.
intros D x eps eps_pos ; eps ; intros ; split.
assumption.
intros y [[_ Hneq] _] ; unfold growth_rate, id ; simpl.
apply Rle_lt_trans with (Rabs 0) ; [| rewrite Rabs_R0 ; assumption].
right ; apply Rabs_eq_compat ; field ; apply Rminus_eq_contra ;
symmetry ; assumption.
Qed.

Lemma derivable_pt_in_id: (D : RProp) (x : R),
derivable_pt_in D id x.
Proof.
intros ; eexists ; eapply derivable_pt_lim_in_id.
Qed.

Lemma derivable_in_id: (D : RProp),
derivable_in D id.
Proof.
intros D x x_in ; eapply derivable_pt_in_id.
Qed.

Lemma derive_pt_open_interval_id : a b x pr,
open_interval a b x
(derive_pt_in (open_interval a b) id x pr = 1)%R.
intros a b x pr x_in ; rewrite derive_open_interval_pt with (pr' := derivable_pt_id x).
apply derive_pt_id.
assumption.
Qed.

Powers

Definition Dpow (n : nat) := match n with
| Ofun _ ⇒ 0
| S mfun x(INR (S m)) × pow x m
end.

Monomials
Inverse
Negative powers