proposition: Lemma binary_round_aux_equiv sx mx ex lx : SpecFloat.binary_round_aux prec emax sx mx ex lx = binary_round_aux prec emax mode_NE sx mx ex lx.
proof: Proof. unfold SpecFloat.binary_round_aux, binary_round_aux. set (mrse' := shr_fexp _ _ _). case mrse'; intros mrs' e'; simpl. now rewrite (round_nearest_even_equiv sx). Qed.
imports: Int63Compat Coq(ZArith Reals Floats SpecFloat) Zaux BinarySingleNaN