proposition: Lemma Halfeps_trans : forall x y z : IR, x[-]Halfeps [<=] y -> y[-]Halfeps [<=] z -> x[-]eps [<=] z.
proof: Proof. intros. astepl (x[-]Halfeps[-]Halfeps). apply leEq_transitive with (y[-]Halfeps). apply minus_resp_leEq. auto. auto. Qed.
imports: Coq.ZArith.ZArith Coq.Arith.Compare CoRN.reals.NRootIR Coq(Lia)