proposition: Lemma Weak_IVT_ap_rht : forall Ha Hb (HFab : F b Hb [<] F a Ha) e, [0] [<] e -> forall z, Compact (less_leEq _ _ _ HFab) z -> {x : IR | Compact Hab x | forall Hx, AbsIR (F x Hx[-]z) [<=] e}.
proof: Proof. intros Ha Hb HFab e H z H0. set (G := {--}F) in *. assert (contG : Continuous_I Hab G). unfold G in |- *; Contin. assert (HGab : G a Ha [<] G b Hb). unfold G in |- *; simpl in |- *; apply inv_resp_less; auto. assert (H1 : Compact (less_leEq _ _ _ HGab) [--]z). inversion_clear H0; split; unfold G in |- *; simpl in |- *; apply inv_resp_leEq; auto. elim (Weak_IVT_ap_lft _ _ _ _ contG _ _ HGab _ H _ H1); intros x Hx. exists x; auto. intro; eapply leEq_wdl. apply (q Hx0). eapply eq_transitive_unfolded. apply AbsIR_minus. apply AbsIR_wd; unfold G in |- *; simpl in |- *; rational. Qed.
imports: CoRN.ftc.Continuity