proposition: Lemma L1ball_closed : forall e x y, (forall d, Qlt 0 d -> (L1Ball (e+d) x y)) -> (L1Ball e x y).
proof: Proof. unfold L1Ball. intros e a b H. assert (forall x, (forall d : Qpos, x <= e+ proj1_sig d) -> x <= e)%Q. { intros. apply: shift_zero_leEq_minus'. apply inv_cancel_leEq. apply approach_zero_weak. intros. replace LHS with (x[-]e). apply: shift_minus_leEq;simpl. replace RHS with (e+ e0)%Q by simpl; ring. exact (H0 (exist _ _ X)). unfold cg_minus; simpl; ring. } apply H0. intros [d dpos]. apply H, dpos. 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