proposition: Lemma decreasing_growing : forall Un:nat -> R, Un_decreasing Un -> Un_growing (opp_seq Un).
proof: Proof. intro. unfold Un_growing, opp_seq, Un_decreasing. intros. apply Ropp_le_contravar. apply H. Qed.
imports: Rbase Rfunctions Rseries Lia