proposition: Lemma valid_ub_correct : forall f, valid_ub f = match classify f with Fminfty => false | _ => true end.
proof: Proof. intro f. unfold valid_ub. rewrite eqb_spec. unfold classify. rewrite classify_spec. unfold SF64classify, SFclassify. case Prim2SF; [now intros [ | ]..|now simpl| ]. now intros [ | ] m e; case Pos.eqb. Qed.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig