proposition: Lemma Rser_rem_lt_le : forall Un lu lv (n : nat) Vn (Hlu : Rser_cv Un lu) (Hlv : Rser_cv Vn lv), (forall k, (k > n)%nat -> Un k <= Vn k) -> {k | (k > n)%nat /\ Un k < Vn k} -> Rser_rem Un lu Hlu n < Rser_rem Vn lv Hlv n.
proof: Proof. intros Un lu lv n Vn Hlu Hlv Hle Hlt. assert (Rser_cv (Vn - Un)%Rseq (lv - lu)). apply Rser_cv_minus_compat ; assumption. assert (Hpos : (forall k, (k > n)%nat -> Vn k - Un k >= 0)). intros. apply Rge_minus. apply Rle_ge. apply Hle. assumption. apply Rminus_gt. generalize (Rser_rem_minus_compat Vn Un lv lu Hlv Hlu H n). intros Hrewrite. unfold Rseq_minus in Hrewrite. rewrite Hrewrite. apply Rser_rem_pos. apply Hpos. destruct Hlt as [k [Hkn Hlt]]. exists k. split. apply Hkn. apply Rgt_minus. apply Hlt. 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