proposition: Lemma W_even_pos : forall n, 0 < W_even n.
proof: Proof. intro n. unfold W_even, Rsqr, Rdiv. repeat apply Rmult_lt_0_compat; try lra. now apply Rlt_le_trans with (7 / 8); lra || apply pi2_int. now apply INR_fact_lt_0. repeat rewrite Rinv_mult_distr ; repeat apply Rmult_lt_0_compat. rewrite Rinv_pow. apply pow_lt ; lra. apply Rgt_not_eq ; lra. apply Rinv_0_lt_compat, pow_lt, INR_fact_lt_0. apply Rgt_not_eq, pow_lt ; lra. apply Rgt_not_eq, pow_lt, INR_fact_lt_0. Qed.
imports: PeanoNat Reals Rintegral Rintegral_usual Rintegral_tactic Lia Lra Rsequence_facts Rsequence_subsequence Rpser RTaylor MyRfunctions Rsequence_tactics