proposition: Lemma Wallis_1 : Rint (sin_n 1) 0 (PI/2) 1.
proof: Proof. unfold sin_n. apply Rint_eq_compat with sin. auto with *. assert(Heq : 1 = (cos 0 - cos (PI/2))). rewrite cos_PI2, cos_0; ring. apply Rint_eq with (cos 0 - cos (PI / 2)) ; auto with Rint. Qed.
imports: PeanoNat Reals Rintegral Rintegral_usual Rintegral_tactic Lia Lra Rsequence_facts Rsequence_subsequence Rpser RTaylor MyRfunctions Rsequence_tactics