proposition: Lemma SubEqui_P1 : forall (a b:R) (del:posreal) (h:a < b), pos_Rl (SubEqui del h) 0 = a.
proof: Proof. intros; unfold SubEqui; case (maxN del h); intros; reflexivity. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra