proposition: Lemma closeRationalLR : forall (a b x d : IR) (Hab : a [<] b), (Compact (less_leEq _ _ _ Hab)) x -> [0][<]d -> {q : Q | (Compact (less_leEq _ _ _ Hab)) q /\ AbsIR (x[-]q)[<=]d}.
proof: Proof. intros ? ? ? ? ? Hcc Hdp. pose proof Hab as Hap. apply less_cotransitive_unfolded with (z:=x)in Hap. destruct Hap as [Hlt | Hgt]. - apply closeRationalL; auto. - apply closeRationalR; auto. 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