proposition: Lemma Lim_mult (f g : R -> R) (x : Rbar) : ex_lim f x -> ex_lim g x -> ex_Rbar_mult (Lim f x) (Lim g x) -> Lim (fun y => f y * g y) x = Rbar_mult (Lim f x) (Lim g x).
proof: Proof. move => /Lim_correct Hf /Lim_correct Hg Hl. apply is_lim_unique. now apply is_lim_mult. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq