proposition: Lemma SubEqui_P5 : forall (a b:R) (del:posreal) (h:a < b), length (SubEqui del h) = S (S (max_N del h)).
proof: Proof. intros; unfold SubEqui; apply SubEqui_P3. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra