proposition: Lemma C0_extension_left {T : UniformSpace} (f : R -> T) la (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)) -> {g : R -> T | (forall c, c < b -> filterlim g (locally c) (locally (g c))) /\ (forall c : R, a < c -> g c = f c) /\ g a = la}.
proof: Proof. intros. destruct (C0_extension_right (fun x => f (- x)) la (-b) (-a)) as [g Hg]. by apply Ropp_lt_contravar. intros. eapply filterlim_comp. apply (filterlim_opp c). apply H0. split ; apply Ropp_lt_cancel ; rewrite Ropp_involutive ; by apply H2. eapply filterlim_comp. apply filterlim_Ropp_left. by rewrite Ropp_involutive. exists (fun x => g (- x)) ; split. intros c Hc. eapply filterlim_comp. apply (filterlim_opp c). by apply Hg, Ropp_lt_contravar. split. intros c Hc. rewrite (proj1 (proj2 Hg)). by rewrite Ropp_involutive. by apply Ropp_lt_contravar. by apply Hg. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq