proposition: Lemma RiemannInt_integrable_eq_compat : forall f g a b, (forall x, f x = g x) -> Riemann_integrable f a b -> Riemann_integrable g a b.
proof: Proof. intros f g a b H X eps. elim X with eps;intros x p; exists x. elim p; intros x0 [p01 p02]; exists x0. split; intros; [ rewrite <- (H t); apply p01 | ]; assumption. Qed.
imports: PeanoNat Reals Lra RiemannInt Rfunction_classes_def Rextensionality