proposition: Lemma ex_lim_minus (f g : R -> R) (x : Rbar) : ex_lim f x -> ex_lim g x -> ex_Rbar_minus (Lim f x) (Lim g x) -> ex_lim (fun y => f y - g y) x.
proof: Proof. move => Hf Hg Hl. apply ex_lim_plus. by apply Hf. apply ex_lim_opp. by apply Hg. rewrite Lim_opp. by apply Hl. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq