fact: Definition nearbyint mode (f : type) := match f with | Fnan => f | Float m e => match mantissa_sign m with | Mnumber s m => round_at_exp_aux mode exponent_zero s m e pos_Eq | Mzero => zero end end.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig