proposition: Lemma equivFloat_Nearbyint {Tl} : forall (t : ArithExpr Tl BinFloat) (lC : evalExprTypeFloat_list Tl) md, let lM := C2M_list lC in eqExprTypeFloat (evalFloat t lC md) (evalRounded t lM md) -> eqExprTypeFloat (evalFloat (Nearbyint t) lC md) (evalRounded (Nearbyint t) lM md).
proof: Proof. intros t lC md lM [fint eqt]. generalize (Bnearbyint_correct _ _ HPrec_lt_emax mode_NE (evalFloat t lC md)). unfold eqExprTypeFloat. simpl. intros [H0 [H1 _]]. unfold FPnearbyint. rewrite H1, H0. now split; [| rewrite <-eqt]. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)