proposition: Lemma SubEqui_P8 : forall (a b:R) (del:posreal) (h:a < b) (i:nat), (i < length (SubEqui del h))%nat -> a <= pos_Rl (SubEqui del h) i <= b.
proof: Proof. intros; split. { pattern a at 1; rewrite <- (SubEqui_P1 del h); apply RList_P5. { apply SubEqui_P7. } elim (RList_P3 (SubEqui del h) (pos_Rl (SubEqui del h) i)); intros; apply H1; exists i; split; [ reflexivity | assumption ]. } pattern b at 2; rewrite <- (SubEqui_P2 del h); apply RList_P7; [ apply SubEqui_P7 | elim (RList_P3 (SubEqui del h) (pos_Rl (SubEqui del h) i)); intros; apply H1; exists i; split; [ reflexivity | assumption ] ]. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra