proposition: Lemma integrable_sin_n : forall n, Riemann_integrable (comp (fun x => pow x n) sin) 0 (PI/2).
proof: Proof. intro n. apply RiemannInt_P6. pose proof PI_RGT_0; lra. intros x Hx; apply continuity_pt_comp. apply continuity_sin. apply derivable_continuous; apply derivable_pow. Qed.
imports: PeanoNat Reals Rintegral Rintegral_usual Rintegral_tactic Lia Lra Rsequence_facts Rsequence_subsequence Rpser RTaylor MyRfunctions Rsequence_tactics