proposition: Lemma Wallis_0 : Rint (sin_n 0) 0 (PI/2) (PI/2).
proof: Proof. apply Rint_eq_compat with (fct_cte 1). trivial. assert(Hrew : (PI/2) = (1*(PI/2 -0))) by ring. apply Rint_eq with (1 * (PI / 2 - 0)). auto with Rint. ring. Qed.
imports: PeanoNat Reals Rintegral Rintegral_usual Rintegral_tactic Lia Lra Rsequence_facts Rsequence_subsequence Rpser RTaylor MyRfunctions Rsequence_tactics