proposition: Lemma ex_lim_div (f g : R -> R) (x : Rbar) : ex_lim f x -> ex_lim g x -> Lim g x <> 0 -> ex_Rbar_div (Lim f x) (Lim g x) -> ex_lim (fun y => f y / g y) x.
proof: Proof. move => Hf Hg Hlg Hl. apply ex_lim_mult ; try assumption. now apply ex_lim_inv. now rewrite Lim_inv. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq