proposition: Lemma RiemannInt_primitive : forall (f:R -> R) (a b:R) (h:a <= b) (pr:forall x:R, a <= x -> x <= b -> Riemann_integrable f a x) (pr0:Riemann_integrable f a b), RiemannInt pr0 = primitive h pr b - primitive h pr a.
proof: Proof. apply RiemannInt_P20. Qed.
imports: PeanoNat Reals Lra RiemannInt Rfunction_classes_def Rextensionality