proposition: Lemma is_lim_minus (f g : R -> R) (x lf lg l : Rbar) : is_lim f x lf -> is_lim g x lg -> is_Rbar_minus lf lg l -> is_lim (fun y => f y - g y) x l.
proof: Proof. move => Hf Hg Hl. eapply is_lim_plus ; try eassumption. now apply is_lim_opp. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq