proposition: Lemma decreasing_ineq : forall (Un:nat -> R) (l:R), Un_decreasing Un -> Un_cv Un l -> forall n:nat, l <= Un n.
proof: Proof. intros. assert (H1 := decreasing_growing _ H). assert (H2 := CV_opp _ _ H0). assert (H3 := growing_ineq _ _ H1 H2). apply Ropp_le_cancel. unfold opp_seq in H3; apply H3. Qed.
imports: Rbase Rfunctions Rseries Lia