proposition: Lemma SubEqui_P7 : forall (a b:R) (del:posreal) (h:a < b), ordered_Rlist (SubEqui del h).
proof: Proof. intros; unfold ordered_Rlist; intros; rewrite SubEqui_P5 in H; simpl in H; inversion H. { rewrite (SubEqui_P6 del h (i:=(max_N del h))). { replace (S (max_N del h)) with (pred (length (SubEqui del h))). { rewrite SubEqui_P2; unfold max_N; case (maxN del h) as (?&?&?); left; assumption. } rewrite SubEqui_P5; reflexivity. } apply Nat.lt_succ_diag_r. } repeat rewrite SubEqui_P6. 3: assumption. 2: apply Nat.lt_succ_r; assumption. apply Rplus_le_compat_l; rewrite S_INR; rewrite Rmult_plus_distr_r; pattern (INR i * del) at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; rewrite Rmult_1_l; left; apply (cond_pos del). Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra