proposition: Lemma RiemannInt_const : forall (c a b : R) (pr : Riemann_integrable (fun x => c) a b), RiemannInt pr = c * (b-a).
proof: Proof. intros. apply RiemannInt_P15. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)