proposition: Lemma is_RInt_ge_0 (f : R -> R) (a b If : R) : a <= b -> is_RInt f a b If -> (forall x, a < x < b -> 0 <= f x) -> 0 <= If.
proof: Proof. intros Hab HIf Hf. set (f' := fun x => if Rle_dec x a then 0 else if Rle_dec b x then 0 else f x). apply is_RInt_ext with (g := f') in HIf. apply closed_filterlim_loc with (1 := HIf) (3 := closed_ge 0). unfold Riemann_fine, within. apply filter_forall. intros ptd Hptd. replace 0 with (scal (sign (b - a)) (Riemann_sum (fun _ => 0) ptd)). apply Rmult_le_compat_l. apply sign_ge_0. now apply Rge_le, Rge_minus, Rle_ge. apply Riemann_sum_le. apply Hptd. intros t _. unfold f'. case Rle_dec as [H1|H1]. apply Rle_refl. case Rle_dec as [H2|H2]. apply Rle_refl. apply Hf. now split; apply Rnot_le_lt. rewrite Riemann_sum_const. by rewrite !scal_zero_r. rewrite (Rmin_left _ _ Hab) (Rmax_right _ _ Hab). intros x Hx. unfold f'. case Rle_dec as [H1|H1]. now elim (Rle_not_lt _ _ H1). case Rle_dec as [H2|H2]. now elim (Rle_not_lt _ _ H2). easy. Qed.
imports: Coq(Reals Psatz) mathcomp(ssreflect ssrbool ssrfun eqtype seq) Markov Rcomplements Rbar Lub Lim_seq SF_seq Continuity Hierarchy