proposition: Lemma Rseq_bound_opp : Rseq_bound (- Un) lu.
proof: Proof. intro n ; unfold Rseq_opp ; rewrite Rabs_Ropp ; apply Un_bd. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_sums_facts Rsequence_rewrite_facts Lra MyRIneq