proposition: Lemma SubEqui_P3 : forall (N:nat) (a b:R) (del:posreal), length (SubEquiN N a b del) = S N.
proof: Proof. simple induction N; intros; [ reflexivity | simpl; rewrite H; reflexivity ]. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra