proposition: Lemma Bessel1_seq_neq_0 (n : nat) : forall k, Bessel1_seq n k <> 0.
proof: Proof. move => k. apply Rmult_integral_contrapositive_currified. apply pow_nonzero, Ropp_neq_0_compat, R1_neq_R0. apply Rinv_neq_0_compat, Rmult_integral_contrapositive_currified ; apply INR_fact_neq_0. Qed.
imports: Coq(Reals Psatz ssreflect) Coquelicot(Rcomplements Rbar Hierarchy Derive Series PSeries Lim_seq AutoDerive)