proposition: Lemma Riemann_integrable_PI : forall (f:R -> R) (a b:R) (pr1 pr2:Riemann_integrable f a b), RiemannInt pr1 = RiemannInt pr2.
proof: Proof. apply RiemannInt_P5. Qed.
imports: PeanoNat Reals Lra RiemannInt Rfunction_classes_def Rextensionality