proposition: Lemma round_nearest_even_equiv s m l : round_nearest_even m l = choice_mode mode_NE s m l.
proof: Proof. case l; [reflexivity|intro c]. case c; [ | reflexivity..]. now simpl; unfold Round.cond_incr; case Z.even. Qed.
imports: Int63Compat Coq(ZArith Reals Floats SpecFloat) Zaux BinarySingleNaN