proposition: Lemma Riemann_integrable_ext : forall (f g : R -> R) (a b : R), (forall x, Rmin a b <= x <= Rmax a b -> f x = g x) -> Riemann_integrable f a b -> Riemann_integrable g a b.
proof: Proof. intros f g a b Heq pr_f. intro eps. elim (pr_f eps) ; clear pr_f ; intros phi (psi, pr_f). exists phi. exists psi. split ; intros. rewrite <- (Heq t H). apply (proj1 pr_f t H). apply pr_f. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)