proposition: Lemma Wallis_quotient_lim1 : Rseq_cv (fun n => W_odd n / W_even n) 1.
proof: Proof. apply Rseq_sandwich_theorem with (Un := fun (n : nat) => 2 * n / (S (2 * n))) (Wn := fun n => 1). apply Rseq_cv_eq_compat with (Un := fun n => 2 * n / (2 * n + 1)). intros n. rewrite S_INR; rewrite mult_INR; reflexivity. apply Rseq_equiv_cv_div. apply Rseq_equiv_sym. apply Rseq_equiv_plus_little_O_compat_l. apply Rseq_equiv_refl. apply Rseq_little_O_Rmult_compat_r; [|intro H; lra]. eapply Rseq_little_O_eq_compat with (Un := Rseq_poly 0) (Vn := Rseq_poly 1). intros n; unfold Rseq_poly; apply pow_O. intros n; unfold Rseq_poly; apply pow_1. apply Rseq_poly_little_O; constructor. intros n; assert (H := pos_INR n); intros Hc; lra. apply Rseq_constant_cv. apply Wallis_bound. Qed.
imports: PeanoNat Reals Rintegral Rintegral_usual Rintegral_tactic Lia Lra Rsequence_facts Rsequence_subsequence Rpser RTaylor MyRfunctions Rsequence_tactics