Interval_premetric@{i} `{!PreMetric@{UA i} A} a b : PreMetric@{UA i} (Interval a b). Proof. split. - unfold close;simpl. apply _. - intros e u. red;red. reflexivity. - intros e u v xi;red;red;symmetry;apply xi. - intros u v E. apply Sigma.path_sigma_hprop. apply separated,E. - intros u v w e d xi1 xi2. red;red. apply (triangular _ (interval_proj a b v)). + exact xi1. + exact xi2. - intros e u v. split. + intros xi. do 2 red in xi. apply (fst (rounded _ _ _)) in xi. exact xi. + intros E. unfold close,Interval_close in E. apply (snd (rounded _ _ _)) in E. exact E. Qed.
Require Import Import NatPair.Instances. Import Quoting.Instances.