proposition: Lemma Rint_eq_compat : forall f g a b x, (forall x, Rmin a b <= x <= Rmax a b -> g x = f x) -> Rint f a b x -> Rint g a b x.
proof: Proof. intros f g a b x Heq. case(Rle_dec a b); intros Hab. intros [prf Hf]. pose proof (Riemann_integrable_eq_compat f g a b Heq prf) as prg. exists prg. erewrite RiemannInt_P18. apply Hf. apply Hab. rewrite (Rmin_def _ _ Hab), (Rmax_def _ _ Hab) in Heq. intuition. rewrite Rmin_comm, Rmax_comm in Heq. intro RIf. apply Rint_reverse_1. apply Rint_reverse_2 in RIf. destruct RIf as [prf Hf]. pose proof (Riemann_integrable_eq_compat f g b a Heq prf) as prg. exists prg. apply Rnot_le_lt, Rlt_le in Hab. erewrite RiemannInt_P18. apply Hf. apply Hab. rewrite (Rmin_def _ _ Hab), (Rmax_def _ _ Hab) in Heq. intuition. Qed.
imports: Reals RiemannInt RIneq Lra R_sqr MyRfunctions