proposition: Lemma Wallis_even : forall n, Rint (sin_n (2 * n)) 0 (PI/2) (W_even n).
proof: Proof. unfold W_even. induction n. simpl; unfold Rsqr; field_simplify; apply Wallis_0. apply Rint_eq_compat with (sin_n (S (S (2 * n)))). intros; simpl; replace (S (n + S (n + 0))) with (S (S (n + (n + 0)))) by auto; reflexivity. replace (PI / 2 * fact (2 * S n) / (2 ^ (2 * S n) * (fact (S n)) ^2)) with ((PI / 2 * fact (2 * n) / (2 ^ (2 * n) * (fact n)^2)) * S (2 * n) / (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; apply fact_neq_0. auto with *. apply pow_nonzero; pose proof Rlt_R0_R2; intro; lra. Qed.
imports: PeanoNat Reals Rintegral Rintegral_usual Rintegral_tactic Lia Lra Rsequence_facts Rsequence_subsequence Rpser RTaylor MyRfunctions Rsequence_tactics