proposition: Lemma RiemannInt_constant : forall (a b c:R) (pr:Riemann_integrable (fct_cte c) a b), RiemannInt pr = c * (b - a).
proof: Proof. apply RiemannInt_P15. Qed.
imports: PeanoNat Reals Lra RiemannInt Rfunction_classes_def Rextensionality