proposition: Lemma derive_pt_D_in : forall f (df:R -> R) (x:R) (pr:derivable_pt f x), D_in f df no_cond x <-> derive_pt f x pr = df x.
proof: Proof. intros; split. - unfold D_in; unfold limit1_in; unfold limit_in; simpl; unfold Rdist; intros. apply derive_pt_eq_0. unfold derivable_pt_lim. intros; elim (H eps H0); intros alpha H1; elim H1; intros; exists (mkposreal alpha H2); intros; generalize (H3 (x + h)); intro; cut (x + h - x = h); [ intro; cut (D_x no_cond x (x + h) /\ Rabs (x + h - x) < alpha); [ intro; generalize (H6 H8); rewrite H7; intro; assumption | split; [ unfold D_x; split; [ unfold no_cond; trivial | symmetry; apply Rminus_not_eq; rewrite H7; assumption ] | rewrite H7; assumption ] ] | ring ]. - intro. assert (H0 := derive_pt_eq_1 f x (df x) pr H). unfold D_in; unfold limit1_in; unfold limit_in; unfold dist; simpl; unfold Rdist; intros. elim (H0 eps H1); intros alpha H2; exists (pos alpha); split. + apply (cond_pos alpha). + intros; elim H3; intros; unfold D_x in H4; elim H4; intros; cut (x0 - x <> 0). * intro; generalize (H2 (x0 - x) H8 H5); replace (x + (x0 - x)) with x0. -- intro; assumption. -- ring. * auto with real. Qed.
imports: Rbase Rfunctions Rlimit Rderiv