proposition: Lemma CompactIntervalQ_bonus_correct : forall e x, In x (approximate CompactIntervalQ e) -> (l <= x <= r).
proof: Proof. intros [e|] x H. simpl in H. eapply UniformPartition_inside. apply H. elim H. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.metric2.Compact CoRN.metric2.LocatedSubset CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs CoRN.model.metric2.Qmetric Coq.QArith.Qround Coq.QArith.Qabs CoRN.model.totalorder.QMinMax CoRN.logic.Classic