proposition: Lemma Wallis_odd : forall n, Rint (sin_n (S (2 * n))) 0 (PI/2) ((2^(2*n) * (fact n) ^2)/(fact (S (2 * n)))).
proof: Proof. unfold W_odd. induction n. simpl; replace (1 * (1 * (1*1)) / 1) with 1 by field; apply Wallis_1. apply Rint_eq_compat with (sin_n (S (S (S (2 * n))))). intros; simpl. replace (n + S (n + 0))%nat with (S (n + (n + 0))) by auto; reflexivity. replace (2 ^ (2 * S n) * (fact (S n))^2 / fact (S (2 * S n))) with ((2 ^ (2 * n) * (fact n)^2 / fact (S (2 * n))) * (S (S (2 * n)))/(S (S (S (2 * n))))). apply Wallis_formula; apply IHn. replace (2 * S n)%nat with (S (S (2 * n))) by auto with *. repeat rewrite fact_simpl. repeat rewrite <- tech_pow_Rmult. unfold Rsqr. replace (S (S (2*n))) with (2 * (S n))%nat by auto with *. repeat rewrite mult_INR. replace (INR 2) with 2 by trivial; field. repeat split;apply not_0_INR; try (auto with * ). apply fact_neq_0. Qed.
imports: PeanoNat Reals Rintegral Rintegral_usual Rintegral_tactic Lia Lra Rsequence_facts Rsequence_subsequence Rpser RTaylor MyRfunctions Rsequence_tactics