proposition: Lemma PSeries_ext_recip (a b : nat -> R) (n : nat) : Rbar_lt (Finite 0) (CV_radius a) -> Rbar_lt (Finite 0) (CV_radius b) -> locally 0 (fun x => PSeries a x = PSeries b x) -> a n = b n.
proof: Proof. move => Ha Hb Hab. have H : a n * (INR (fact n)) = b n * (INR (fact n)). rewrite -?Derive_n_coef => //. by apply Derive_n_ext_loc. replace (a n) with ((a n * INR (fact n)) / (INR (fact n))). rewrite H ; field ; exact: INR_fact_neq_0. field ; exact: INR_fact_neq_0. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series