proposition: Lemma ProductMS_located : locatedMetric X -> locatedMetric Y -> locatedMetric ProductMS.
proof: Proof. unfold locatedMetric. intros H0 H1 e d x y Hed. destruct (H0 _ _ (fst x) (fst y) Hed) as [A | A]. destruct (H1 _ _ (snd x) (snd y) Hed) as [B | B]. left. split; assumption. right; intros [_ H]. apply B; assumption. right; intros [H _]. apply A; assumption. Defined.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Metric CoRN.metric2.Classification CoRN.metric2.UniformContinuity CoRN.metric2.Prelength CoRN.metric2.Complete CoRN.metric2.LocatedSubset