proposition: Lemma Riemann_integrable_eq_compat : forall f g a b, (forall x, Rmin a b <= x <= Rmax a b -> g x = f x) -> Riemann_integrable f a b -> Riemann_integrable g a b.
proof: Proof. intros f g a b Heq prf; case(Rle_dec a b); intro Hab; [ | apply RiemannInt_P1 in prf; apply RiemannInt_P1]; intro eps; destruct (prf eps) as [phi [psi Hpsi]]; [ | rewrite Rmin_comm, Rmax_comm in Heq ]; exists phi; exists psi. split; [ intros t Ht; rewrite Heq; [ apply Hpsi | apply Ht] ; apply Ht | apply Hpsi ] . split; [ intros t Ht; rewrite Heq; [ apply Hpsi | apply Ht] ; apply Ht | apply Hpsi ] . Qed.
imports: Reals RiemannInt RIneq Lra R_sqr MyRfunctions