proposition: Lemma L1ball_dec : forall e a b, {L1Ball e a b}+{~L1Ball e a b}.
proof: Proof. intros e a b. unfold L1Ball. set (d:=L1Distance a b). destruct (Qlt_le_dec_fast e d) as [Hdc|Hdc]. right. abstract auto with *. left. exact Hdc. Defined.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.structures.StepQsec CoRN.metric2.UniformContinuity CoRN.metric2.Prelength CoRN.model.structures.OpenUnit Coq.QArith.QArith CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.metric2.Qmetric CoRN.algebra.COrdFields2 CoRN.tactics.CornTac