fact: Definition ufloat_pos_Eq beta (x : ufloat beta) := match x with Ufloat _ _ _ pos_Eq => True | Ufloat _ _ _ _ => False | _ => True end.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic