proposition: Lemma L1Ball_e_wd : forall (e1 e2:Q) x y, Qeq e1 e2 -> (L1Ball e1 x y <-> L1Ball e2 x y).
proof: Proof. intros x1 x2 y1 y2 Hx. unfold L1Ball. rewrite -> Hx. reflexivity. 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