fact: Definition unop_nan_pl32 (f : binary32) : { nan : binary32 | is_nan 24 128 nan = true } := match f as f with | B754_nan s pl Hpl => exist _ (B754_nan s pl Hpl) (refl_equal true) | _ => default_nan_pl32 end.
imports: Coq(ZArith Reals Lia SpecFloat) Core BinarySingleNaN Binary