proposition: Lemma Wallis_odd_le_even : forall n, W_odd n <= W_even n.
proof: Proof. intro n. apply (Rint_le_compat (sin_n (S (2 * n))) (sin_n (2 * n)) 0 (PI/2)). left; apply PI2_RGT_0. intros; unfold sin_n. replace (sin u ^ (2 * n)) with (1 * sin u ^ (2 * n)) by ring. rewrite <- tech_pow_Rmult. apply Rmult_le_compat_r. apply pow_le. apply sin_ge_0; intuition; lra. pose proof (SIN_bound u); intuition. apply Wallis_odd. apply Wallis_even. Qed.
imports: PeanoNat Reals Rintegral Rintegral_usual Rintegral_tactic Lia Lra Rsequence_facts Rsequence_subsequence Rpser RTaylor MyRfunctions Rsequence_tactics