proposition: Lemma ProductMS_prelength : PrelengthSpace X -> PrelengthSpace Y -> PrelengthSpace ProductMS.
proof: Proof. intros HX HY a b e d1 d2 Hed Hab. destruct (HX (fst a) (fst b) e d1 d2 Hed (proj1 Hab)) as [c1 Hc1]. destruct (HY (snd a) (snd b) e d1 d2 Hed (proj2 Hab)) as [c2 Hc2]. exists (c1,c2); split; 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