proposition: Lemma ex_Bessel1 (n : nat) (x : R) : ex_pseries (Bessel1_seq n) x.
proof: Proof. apply CV_radius_inside. by rewrite CV_Bessel1. Qed.
imports: Coq(Reals Psatz ssreflect) Coquelicot(Rcomplements Rbar Hierarchy Derive Series PSeries Lim_seq AutoDerive)