proposition: Lemma Halfeps_Halfeps : forall x : IR, x[-]Halfeps[-]Halfeps [=] x[-]eps.
proof: Proof. intros. unfold Halfeps in |- *. unfold Half in |- *. rational. Qed.
imports: Coq.ZArith.ZArith Coq.Arith.Compare CoRN.reals.NRootIR Coq(Lia)