proposition: Lemma Q_is_MetricSpace : is_MetricSpace Qball.
proof: Proof. split; auto with typeclass_instances. - intros e1 e2 a b c H1 H2. unfold Qball. unfold QAbsSmall. simpl. assert (Qeq (a-c) ((a-b)+(b-c))) by ring. rewrite H. clear H. split. apply (Qle_trans _ (-e1 + -e2)). ring_simplify. apply Qle_refl. apply Qplus_le_compat. apply H1. apply H2. apply Qplus_le_compat. apply H1. apply H2. - intros e a b H. split. apply Qle_closed. intros [d dpos]. simpl. specialize (H d dpos). destruct H. apply (Qplus_le_l _ _ (-d)). ring_simplify. simpl in H. ring_simplify in H. exact H. apply Qle_closed. intros. apply H. apply Qpos_ispos. - intros. destruct H. apply (Qle_trans _ _ _ H) in H0. apply (Qplus_le_l _ _ e) in H0. ring_simplify in H0. rewrite <- (Qmult_0_r (2#1)) in H0. apply Qmult_le_l in H0. exact H0. reflexivity. - intros. split. + apply Qnot_lt_le. intro abs. contradict H; intros [H _]. exact (Qlt_not_le _ _ abs H). + apply Qnot_lt_le. intro abs. contradict H; intros [_ H]. exact (Qlt_not_le _ _ abs H). 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