proposition: Lemma SubEqui_P4 : forall (N:nat) (a b:R) (del:posreal) (i:nat), (i < S N)%nat -> pos_Rl (SubEquiN (S N) a b del) i = a + INR i * del.
proof: Proof. simple induction N; [ intros; inversion H; [ simpl; ring | elim (Nat.nle_succ_0 _ H1) ] | intros; induction i as [| i Hreci]; [ simpl; ring | change (pos_Rl (SubEquiN (S n) (a + del) b del) i = a + INR (S i) * del) ; rewrite H; [ rewrite S_INR; ring | apply Nat.succ_lt_mono; apply H0 ] ] ]. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra