proposition: Lemma Halfeps_eps : forall x y : IR, x[-]Halfeps [<=] y -> x[-]eps [<=] y.
proof: Proof. intros. astepl (x[-]Halfeps[-]Halfeps). apply leEq_transitive with (x[-]Halfeps). apply less_leEq. apply shift_minus_less. apply shift_less_plus'. astepl ZeroR. apply Halfeps_pos. auto. Qed.
imports: Coq.ZArith.ZArith Coq.Arith.Compare CoRN.reals.NRootIR Coq(Lia)