proposition: Lemma L1ball_eq : forall x y, (forall e : Q, Qlt 0 e -> L1Ball e x y) -> StepF_eq x y.
proof: Proof. intros x y H. unfold L1Ball in H. setoid_replace y with (constStepF (0:QS)+y); [| ring]. set (z:=constStepF (0:QS)). setoid_replace x with (x - y + y); [| ring]. apply StepQplus_wd; try reflexivity. unfold z; clear z. apply L1Norm_Zero. apply Qnot_lt_le. intro H0. assert (H1:0<(1#2)*( L1Norm (QminusS ^@> x <@> y))). apply: mult_resp_pos; simpl; auto with *. apply: (Qle_not_lt _ _ (H _ H1)). simpl. rewrite -> Qlt_minus_iff. unfold L1Distance. unfold StepQminus. simpl. ring_simplify. assumption. 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