proposition: Lemma Weak_IVTQ : forall (I : interval) (F : PartFunct IR), Continuous I F -> forall (a b : IR) (Ha : Dom F a) (Hb : Dom F b) (HFab : F a Ha[<]F b Hb), I a -> I b -> forall e : IR, [0][<]e -> forall y : IR, Compact (less_leEq IR (F a Ha) (F b Hb) HFab) y -> {x : Q | Compact (Min_leEq_Max a b) x /\ forall Hx : Dom F x, AbsIR (F x Hx[-]y)[<=]e}.
proof: Proof. intros ? ? Hc ? ? ? ? ? Hia Hib ? He ? Hcp. apply pos_div_two in He. pose proof He as Hivt. eapply Weak_IVT with (y:=y) (F:=F) (HFab := HFab) in Hivt; eauto. unfold compact in He. unfold Continuous in Hc. destruct Hc as [Hcl Hcr]. specialize (Hcr _ _ (Min_leEq_Max a b)). unfold Continuous_I in Hcr. match type of Hcr with ?A -> _ => assert A as H99 by (apply included_interval; auto); pose proof (included_trans _ _ _ _ H99 Hcl) as Hdom; specialize (Hcr H99); clear H99 end. apply snd in Hcr. specialize (Hcr _ He). destruct Hcr as [d Hdp Hcc]. destruct Hivt as [x Hmm Hfx]. pose proof HFab as Hap. specialize (fun xp => Hcc x xp Hmm). apply less_imp_ap in Hap. apply pfstrx in Hap. apply ap_imp_Min_less_Max in Hap. pose proof (closeRationalLR _ _ _ _ Hap Hmm Hdp) as Hqq. destruct Hqq as [q H99]. exists q. destruct H99 as [Hcomp Hab]. split;[exact Hcomp|]. specialize (Hcc q Hcomp (Hdom _ Hmm) (Hdom _ Hcomp) Hab). specialize (Hfx (Hdom _ Hmm)). rewrite AbsIR_minus in Hcc. apply AbsIR_imp_AbsSmall in Hcc. apply AbsIR_imp_AbsSmall in Hfx. pose proof (AbsSmall_eps_div_two _ _ _ _ Hcc Hfx) as Hsum. clear Hfx Hcc. unfold cg_minus in Hsum. ring_simplify in Hsum. intros Hx. apply AbsSmall_imp_AbsIR. rewrite pfwdef with (Hy := Hx) in Hsum; trivial. apply eq_reflexive. Qed.
imports: CoRN.ftc.FTC Coq.setoid_ring.Ring CoRN.tactics.CornTac CoRN.algebra.CRing_as_Ring CoRN.ftc.Derivative CoRN.ftc.Integral CoRN.ftc.StrongIVT