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