proposition: Lemma QPrelengthSpace : PrelengthSpace Q_as_MetricSpace.
proof: Proof. intros a b e d1 d2 He Hab. pose ((a * proj1_sig d2 + b * proj1_sig d1) / proj1_sig (d1 + d2)%Qpos) as c. exists c. apply (@QPrelengthSpace_help e d1 d2 He a b c); try assumption. reflexivity. apply ball_sym. eapply QPrelengthSpace_help. rewrite -> Qplus_comm. apply He. apply ball_sym. apply Hab. unfold c. unfold Qdiv. apply Qmult_comp. ring. apply Qinv_comp. simpl. ring. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.Prelength CoRN.metric2.Classification CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax Coq.QArith.Qabs CoRN.metric2.UniformContinuity MathClasses.implementations.stdlib_rationals