proposition: Lemma Wallis_quotient : forall n, W_odd n / W_even n = (2*2 ^ (4*n) * (fact n) ^ 4)/(PI*fact (2 * n) * fact (S (2 * n))).
proof: Proof. intro n; unfold W_odd, W_even, Rsqr, Rdiv. replace (2 ^ (4 * n)) with ((2 ^ (2 * n)) * (2 ^ (2 * n))). field; repeat split. apply not_0_INR; apply fact_neq_0. apply not_0_INR; apply fact_neq_0. apply PI_neq0. apply not_0_INR; apply fact_neq_0. apply pow_nonzero; intros H; lra. replace (4 * n)%nat with (2 * n + 2 * n)%nat by lia. rewrite pow_add. reflexivity. Qed.
imports: PeanoNat Reals Rintegral Rintegral_usual Rintegral_tactic Lia Lra Rsequence_facts Rsequence_subsequence Rpser RTaylor MyRfunctions Rsequence_tactics