proposition: Lemma Rint_sin : forall a b, Rint sin a b (cos a - cos b).
proof: Proof. intros a b. replace (cos a - cos b) with (- cos b - -cos a) by ring. apply Rint_derive2 with (f := (-cos)%F). intros; replace (sin x) with (--sin x) by ring; apply derivable_pt_lim_opp, derivable_pt_lim_cos. intros; apply continuity_sin. Qed.
imports: Reals MyRfunctions Rintegral Lia