proposition: Lemma L1ball_refl : forall e x, Qle 0 e -> (L1Ball e x x).
proof: Proof. intros e x epos. unfold L1Ball, L1Distance. setoid_replace (x-x) with (constStepF (0:QS)); [| ring]. change (0 <= e)%Q. auto with *. Qed.
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