proposition: Lemma Rseq_cv_minus_compat : forall Un Vn lu lv, Rseq_cv Un lu -> Rseq_cv Vn lv -> Rseq_cv (Un - Vn) (lu - lv).
proof: Proof. intros Un Vn lu lv Hlu Hlv. apply Rseq_cv_eq_compat with (Un + (-Vn)). intros n; reflexivity. apply Rseq_cv_plus_compat; [apply Hlu|]. apply Rseq_cv_opp_compat; apply Hlv. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra