proposition: Lemma Wallis_bound : forall (n : nat), 2*n / (S(2 * n)) <= W_odd n / W_even n <= 1.
proof: Proof. intro n ; split. apply Rle_trans with (2 * n / S (2 * n) * (W_even n / W_even n)). right ; field ; split. apply Rgt_not_eq ; apply W_even_pos. apply not_0_INR ; discriminate. unfold Rdiv ; rewrite <- Rmult_assoc ; apply Rmult_le_compat_r. left ; apply Rinv_0_lt_compat ; apply W_even_pos. apply Wallis_maj. rewrite <- Rinv_r with (W_even n). unfold Rdiv ; apply Rmult_le_compat_r. left ; apply Rinv_0_lt_compat ; apply W_even_pos. apply Wallis_odd_le_even. apply Rgt_not_eq ; apply W_even_pos. Qed.
imports: PeanoNat Reals Rintegral Rintegral_usual Rintegral_tactic Lia Lra Rsequence_facts Rsequence_subsequence Rpser RTaylor MyRfunctions Rsequence_tactics