fact: Definition unop_nan_pl64 (f : binary64) : { nan : binary64 | is_nan 53 1024 nan = true } := match f as f with | B754_nan s pl Hpl => exist _ (B754_nan s pl Hpl) (refl_equal true) | _ => default_nan_pl64 end.
imports: Coq(ZArith Reals Lia SpecFloat) Core BinarySingleNaN Binary