proposition: Lemma SubEqui_P6 : forall (a b:R) (del:posreal) (h:a < b) (i:nat), (i < S (max_N del h))%nat -> pos_Rl (SubEqui del h) i = a + INR i * del.
proof: Proof. intros; unfold SubEqui; apply SubEqui_P4; assumption. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra