proposition: Lemma seq_exist_subproof : forall Un Vn n, (forall k, (k > n)%nat -> Vn k <= Un (k - S n)%nat) -> {k | (k > n)%nat /\ Vn k < Un (k - S n)%nat} -> {Wn : (nat -> R)&{k | (forall k1, Vn k1 + Wn k1 = Un (k1 - S n)%nat /\ ((k1 > n)%nat -> Wn k1 >= 0)) /\ (k > n)%nat /\ Wn k > 0}}.
proof: Proof. intros Un Vn n Hle Hlt. pose (Un1 := fun k => Un (k - S n)%nat). pose (Wn := (Un1 - Vn)%Rseq). destruct Hlt as [k [Hnk Hlt]]. exists Wn. exists k. split. unfold Wn. unfold Rseq_minus, Un1; intuition. apply Rge_minus. apply Rle_ge. apply Hle. assumption. split ; [assumption|unfold Wn, Rseq_minus, Un1]. apply Rgt_minus. assumption. Qed.
imports: Reals Rsequence Rseries_def Rseries_base_facts Rseries_pos_facts Rseries_remainder_facts Rseries_cv_facts Rseries_usual Lra PeanoNat Rtactic MyRIneq Rsequence