proposition: Lemma uniform_metric_bound_below (f g : uniform_space) (x : X) : d (proj1_sig f x) (proj1_sig g x) <= uniform_metric f g.
proof: Proof. unfold uniform_metric. destruct f as [f Hf]; destruct g as [g Hg]; destruct sup. simpl. apply i. exists x; trivial; constructor. Qed.
imports: MetricSpaces FunctionalExtensionality Completeness Description Max Psatz Lra