fact: Definition mode_choice mode s m l := match mode with | rnd_UP => cond_incr (round_sign_UP s l) m | rnd_DN => cond_incr (round_sign_DN s l) m | rnd_ZR => m | rnd_NE => cond_incr (round_N (negb (Z.even m)) l) m end.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic