proposition: Lemma SubEqui_P2 : forall (a b:R) (del:posreal) (h:a < b), pos_Rl (SubEqui del h) (pred (length (SubEqui del h))) = b.
proof: Proof. intros; unfold SubEqui; destruct (maxN del h)as (x,_). cut (forall (x:nat) (a:R) (del:posreal), pos_Rl (SubEquiN (S x) a b del) (pred (length (SubEquiN (S x) a b del))) = b); [ intro; apply H | simple induction x0; [ intros; reflexivity | intros; change (pos_Rl (SubEquiN (S n) (a0 + del0) b del0) (pred (length (SubEquiN (S n) (a0 + del0) b del0))) = b) ; apply H ] ]. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra