proposition: Lemma C0_extension_lt {T : UniformSpace} (f : R -> T) la lb (a b : R) : a < b -> (forall c : R, a < c < b -> filterlim f (locally c) (locally (f c))) -> (filterlim f (at_right a) (locally la)) -> (filterlim f (at_left b) (locally lb)) -> {g : R -> T | (forall c, filterlim g (locally c) (locally (g c))) /\ (forall c : R, a < c < b -> g c = f c) /\ g a = la /\ g b = lb}.
proof: Proof. intros. destruct (C0_extension_left f la a b) as [g [Cg [Gab Ga]]] => //. destruct (C0_extension_right g lb a b) as [h [Ch [Hab Hb]]] => //. intros. apply Cg, H3. eapply filterlim_ext_loc. 2: by apply H2. apply Rminus_lt_0 in H. exists (mkposreal _ H) => y /= Hy Hy'. apply sym_eq, Gab. apply Ropp_lt_cancel, (Rplus_lt_reg_l b). eapply Rle_lt_trans, Hy. rewrite -abs_opp opp_minus. apply Rle_abs. exists h ; repeat split. intros c. case: (Rlt_le_dec a c) => Hac. by apply Ch. rewrite Hab. eapply filterlim_ext_loc. 2: apply Cg. apply locally_interval with m_infty b => //. by eapply Rle_lt_trans, H. intros y _ Hy ; by apply sym_eq, Hab. by eapply Rle_lt_trans, H. by eapply Rle_lt_trans, H. intros c [Hac Hcb]. rewrite Hab => //. by apply Gab. by rewrite Hab. by []. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq