proposition: Lemma IVT_Rbar_decr (f : R -> R) (a b la lb : Rbar) (y : R) : is_lim f a la -> is_lim f b lb -> (forall (x : R), Rbar_lt a x -> Rbar_lt x b -> continuity_pt f x) -> Rbar_lt a b -> Rbar_lt lb y /\ Rbar_lt y la -> {x : R | Rbar_lt a x /\ Rbar_lt x b /\ f x = y}.
proof: Proof. move => Hla Hlb Cf Hab Hy. case: (IVT_Rbar_incr (fun x => - f x) a b (Rbar_opp la) (Rbar_opp lb) (-y)). by apply is_lim_opp. by apply is_lim_opp. move => x Hax Hxb. by apply continuity_pt_opp, Cf. by apply Hab. split ; apply Rbar_opp_lt ; rewrite Rbar_opp_involutive /Rbar_opp Ropp_involutive ; by apply Hy. move => x Hx ; exists x ; intuition. by rewrite -(Ropp_involutive y) -H4 Ropp_involutive. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq