proposition: Lemma D_pow_n : forall (n:nat) (D:R -> Prop) (x0:R) (expr dexpr:R -> R), D_in expr dexpr D x0 -> D_in (fun x:R => expr x ^ n) (fun x:R => INR n * expr x ^ (n - 1) * dexpr x) ( Dgf D D expr) x0.
proof: Proof. intros n D x0 expr dexpr H; generalize (Dcomp D D dexpr (fun x:R => INR n * x ^ (n - 1)) expr ( fun x:R => x ^ n) x0 H (Dx_pow_n n D (expr x0))); intro; unfold D_in; unfold limit1_in; unfold limit_in; simpl; intros; unfold D_in in H0; unfold limit1_in in H0; unfold limit_in in H0; simpl in H0; elim (H0 eps H1); clear H0; intros; elim H0; clear H0; intros; split with x; split; intros; auto. cut (dexpr x0 * (INR n * expr x0 ^ (n - 1)) = INR n * expr x0 ^ (n - 1) * dexpr x0); [ intro Rew; rewrite <- Rew; exact (H2 x1 H3) | ring ]. Qed.
imports: Rbase Rfunctions Rlimit Lra Lia