proposition: Lemma derivable_pt_lim_D_in : forall f (df:R -> R) (x:R), D_in f df no_cond x <-> derivable_pt_lim f x (df x).
proof: Proof. intros; split. - unfold D_in; unfold limit1_in; unfold limit_in; simpl; unfold Rdist; intros. 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. unfold derivable_pt_lim in H. unfold D_in; unfold limit1_in; unfold limit_in; unfold dist; simpl; unfold Rdist; intros. elim (H eps H0); intros alpha H2; exists (pos alpha); split. + apply (cond_pos alpha). + intros. elim H1; intros; unfold D_x in H3; elim H3; intros; cut (x0 - x <> 0). * intro; generalize (H2 (x0 - x) H7 H4); replace (x + (x0 - x)) with x0. -- intro; assumption. -- ring. * auto with real. Qed.
imports: Rbase Rfunctions Rlimit Rderiv