proposition: Lemma rseq_limit_opp_is_limit : forall r l, is_limit r l -> is_limit (- r) (rseq_limit_opp l).
proof: Proof. intros r [] Hl ; simpl ; [ apply Rseq_cv_neg_infty_opp_compat | apply Rseq_cv_opp_compat | apply Rseq_cv_pos_infty_opp_compat] ; assumption. Qed.
imports: Rbase MyRIneq Rsequence_def Rsequence_facts Rsequence_cv_facts List Option Tactics