proposition: Lemma compactness_value_1d : forall a b (delta : R -> posreal), { d : posreal | forall x, a <= x <= b -> ~~ exists t, a <= t <= b /\ Rabs (x - t) < delta t /\ d <= delta t }.
proof: Proof. intros a b delta. destruct (compactness_value 1 (a,tt) (b,tt) (fun t => let '(t,_) := t in delta t)) as (d, Hd). exists d. intros x Hx. specialize (Hd (x,tt) (conj Hx I)). do 2 contradict Hd. destruct Hd as ((t,t'),Ht). exists t. repeat split ; apply Ht. Qed.
imports: Coq(Reals List ssreflect) Rcomplements