proposition: Lemma is_RInt_KHInt : forall (f : R -> V) (a b : R) (l : V), is_RInt f a b l -> is_KHInt f a b l.
proof: Proof. intros f a b I. unfold is_RInt, is_KHInt. apply filterlim_filter_le_1. unfold filter_le, Riemann_fine, KH_fine, within, KH_filter, locally_dist. intros P [delta HPdelta]. exists (fun _ => delta). intros ptd Hptd1 Hptd2. apply HPdelta. 2: exact Hptd2. clear -Hptd1 Hptd2. unfold fine in Hptd1. revert Hptd1 Hptd2. assert ((forall i : nat, (i < SF_size ptd)%nat -> ith_step ptd i < delta) -> pointed_subdiv ptd /\ SF_h ptd >= Rmin a b /\ last (SF_h ptd) (SF_lx ptd) = Rmax a b -> seq_step (SF_lx ptd) < delta) as H0. apply SF_cons_ind with (s := ptd) => {ptd} [x0 | h ptd IH] H. intros H0. apply cond_pos. intro H0. rewrite SF_lx_cons. unfold seq_step ; simpl. apply Rmax_case. specialize (H 0%nat). unfold ith_step in H. rewrite SF_lx_cons in H. simpl in H. rewrite Rabs_right. apply H. rewrite SF_size_cons. apply Nat.lt_0_succ. destruct H0 as (H0, H1). unfold pointed_subdiv in H0. apply Rge_minus. apply Rle_ge. specialize (H0 0%nat). apply Rle_trans with (nth 0 (SF_ly (SF_cons h ptd)) 0) ; apply H0 ; rewrite SF_size_cons ; apply Nat.lt_0_succ. apply IH. intros i Hi. specialize (H (S i)). unfold ith_step. unfold ith_step in H. change (nth 0 (SF_lx ptd) (S i)) with (nth 0 (SF_lx (SF_cons h ptd)) (S (S i))). change (nth 0 (SF_lx ptd) i) with (nth 0 (SF_lx (SF_cons h ptd)) (S i)). apply H. rewrite SF_size_cons ; now apply <-Nat.lt_succ_r. split. apply ptd_cons with h. apply H0. split. apply Rge_trans with (SF_h (SF_cons h ptd)). 2:apply H0. 2:apply H0. apply Rle_ge. destruct H0 as (H0, H1). unfold pointed_subdiv in H0. specialize (H0 0%nat). change (SF_h (SF_cons h ptd)) with (nth 0 (SF_lx (SF_cons h ptd)) 0). change (SF_h ptd) with (nth 0 (SF_lx (SF_cons h ptd)) 1). apply Rle_trans with (nth 0 (SF_ly (SF_cons h ptd)) 0) ; apply H0 ; rewrite SF_size_cons ; apply Nat.lt_0_succ. intros H1 H2. apply H0. apply H1. split. apply H2. split. destruct H2 as (H2, (H3, H4)). rewrite H3. apply Rge_refl. apply H2. Qed.
imports: Coq(Reals ssreflect ssrbool) mathcomp(seq) Rcomplements Hierarchy SF_seq RInt