proposition: Lemma RiemannInt_singleton : forall (f:R -> R) (a:R) (pr:Riemann_integrable f a a), RiemannInt pr = 0.
proof: Proof. apply RiemannInt_P9. Qed.
imports: PeanoNat Reals Lra RiemannInt Rfunction_classes_def Rextensionality