proposition: Lemma is_lim_mult (f g : R -> R) (x lf lg : Rbar) : is_lim f x lf -> is_lim g x lg -> ex_Rbar_mult lf lg -> is_lim (fun y => f y * g y) x (Rbar_mult lf lg).
proof: Proof. intros Cf Cg Hp. eapply filterlim_comp_2 ; try eassumption. by apply filterlim_Rbar_mult, Rbar_mult_correct. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq