proposition: Lemma Interval_premetric@{i} `{!PreMetric@{UA i} A} a b : PreMetric@{UA i} (Interval a b).
proof: 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.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.rationals HoTT.Classes.interfaces.orders HoTT.Classes.implementations.peano_naturals HoTT.Classes.implementations.natpair_integers HoTT.Classes.theory.groups HoTT.Classes.theory.integers HoTT.Classes.theory.dec_fields HoTT.Classes.orders.dec_fields HoTT.Classes.orders.sum HoTT.Classes.theory.rationals HoTT.Classes.orders.lattices HoTT.Classes.implementations.assume_rationals HoTT.Classes.tactics.ring_quote HoTT.Classes.tactics.ring_tac