proposition: Lemma is_derive_Reals (f : R -> R) (x l : R) : is_derive f x l <-> derivable_pt_lim f x l.
proof: Proof. apply iff_sym. split => Hf. + split. apply @is_linear_scal_l. simpl => y Hy eps. rewrite -(is_filter_lim_locally_unique _ _ Hy) ; clear y Hy. case: (Hf eps (cond_pos _)) => {Hf} d Hf. exists d => y /= Hy. case: (Req_dec y x) => Hxy. rewrite Hxy /norm /scal /= /abs /minus /plus /opp /mult /=. ring_simplify (f x + - f x + - ((x + - x) * l)). ring_simplify (x + - x). rewrite Rabs_R0 Rmult_0_r. by apply Rle_refl. apply Rle_div_l. apply Rabs_pos_lt. by apply Rminus_eq_contra. rewrite -Rabs_div. 2: by apply Rminus_eq_contra. rewrite /scal /= /minus /plus /opp /mult /=. replace ((f y + - f x + - ((y + - x) * l)) / (y + - x)) with ((f (x + (y-x)) - f x) / (y-x) - l). 2: ring_simplify (x + (y - x)) ; field ; by apply Rminus_eq_contra. apply Rlt_le, Hf. by apply Rminus_eq_contra. by []. + move => e He. destruct Hf as [_ Hf]. specialize (Hf x (fun P H => H)). destruct (Hf (pos_div_2 (mkposreal _ He))) as [delta Hd]. exists delta => h Hh0 Hh. apply Rle_lt_trans with (e / 2). simpl in Hd. replace ((f (x + h) - f x) / h - l) with ((f (x + h) + - f x + - ((x + h + - x) * l)) / (x + h + - x)). 2: by field. rewrite Rabs_div. 2: by ring_simplify (x + h + - x). apply Rle_div_l. now ring_simplify (x + h + - x) ; apply Rabs_pos_lt. apply Hd. rewrite /ball /= /AbsRing_ball /= /abs /minus /plus /opp /=. by ring_simplify (x + h + - x). apply Rlt_div_l, Rminus_lt_0 ; ring_simplify. by apply Rlt_0_2. by []. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv