proposition: Lemma Lim_seq_minus (u v : nat -> R) : ex_lim_seq u -> ex_lim_seq v -> ex_Rbar_minus (Lim_seq u) (Lim_seq v) -> Lim_seq (fun n => u n - v n) = Rbar_minus (Lim_seq u) (Lim_seq v).
proof: Proof. intros Hu Hv Hl. apply is_lim_seq_unique. eapply is_lim_seq_minus ; try apply Lim_seq_correct ; try assumption. by apply Rbar_plus_correct. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy