proposition: Lemma binary_round_equiv s m e : SpecFloat.binary_round prec emax s m e = binary_round prec emax mode_NE s m e.
proof: Proof. unfold SpecFloat.binary_round, binary_round, shl_align_fexp. set (mez := shl_align _ _ _); case mez as [mz ez]. apply binary_round_aux_equiv. Qed.
imports: Int63Compat Coq(ZArith Reals Floats SpecFloat) Zaux BinarySingleNaN