proposition: Lemma RiemannInt_ext : forall (f g : R -> R) (a b : R) (pr_f : Riemann_integrable f a b) (pr_g : Riemann_integrable g a b) (Heq : forall x, Rmin a b <= x <= Rmax a b -> f x = g x), RiemannInt pr_f = RiemannInt pr_g.
proof: Proof. intros. destruct (Rle_lt_dec a b). apply RiemannInt_P18. apply r. intros. apply Heq. split. rewrite (Rmin_left _ _ r). apply Rlt_le ; apply H. rewrite (Rmax_right _ _ r). apply Rlt_le ; apply H. rewrite (RiemannInt_P8 pr_f (RiemannInt_P1 pr_f)). rewrite (RiemannInt_P8 pr_g (RiemannInt_P1 pr_g)). apply Ropp_eq_compat. apply RiemannInt_P18. apply Rlt_le ; apply r. intros. apply Heq. split. rewrite (Rmin_right _ _ (Rlt_le _ _ r)). apply Rlt_le ; apply H. rewrite (Rmax_left _ _ (Rlt_le _ _ r)). apply Rlt_le ; apply H. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)