proposition: Lemma Wallis_maj : forall n : nat, (2*n/ (S (2 * n))) * (W_even n) <= W_odd n.
proof: Proof. intro n. destruct n. unfold W_even, W_odd, Rsqr. simpl; field_simplify; lra. replace 2 with (INR 2) by trivial; rewrite <- mult_INR. replace (2 * S n)%nat with (S (S (2 * n))) by auto with *. replace (W_odd (S n)) with (INR (S (S (2 * n))) / INR (S (S (S (2 * n)))) * W_odd n). apply Rmult_le_compat_l. unfold Rdiv. repeat apply Rmult_le_pos; auto with *. apply Wallis_even_le_odd. rewrite Rmult_comm. unfold Rdiv. rewrite <- Rmult_assoc. eapply (Rint_uniqueness _ 0 (PI/2)). apply Wallis_formula. apply Wallis_odd. replace (S (S (2 * n))) with (2 * (S n))%nat by auto with *. apply Wallis_odd. Qed.
imports: PeanoNat Reals Rintegral Rintegral_usual Rintegral_tactic Lia Lra Rsequence_facts Rsequence_subsequence Rpser RTaylor MyRfunctions Rsequence_tactics