proposition: Lemma ball_Cunit : forall (e:Q) a b, ball e (Cunit a) (Cunit b) <-> ball e a b.
proof: Proof. intros e a b. split. - intros. simpl in H. do 2 (apply ball_closed; intros). rewrite <- (Qplus_comm d). apply (H (exist _ _ H0) (exist _ _ H1)). - intros H d1 d2. pose proof (msp_nonneg (msp X) _ _ _ H). apply Qle_lteq in H0. destruct H0. apply (Cunit_prf (exist _ _ H0)). exact H. rewrite <- H0, Qplus_0_r. rewrite <- H0 in H. simpl. rewrite H. apply ball_refl. apply (Qpos_nonneg (d1+d2)). Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax