proposition: Lemma UtoX_pos_Eq : forall beta (x : ufloat beta), (UtoX x = Xnan -> x = Unan) -> ufloat_pos_Eq beta x.
proof: Proof. now intros beta [| |s m e [| | |]] H ; try exact I ; specialize (H (refl_equal _)). Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic