fact: Definition is_finite_FF f := match f with | F754_finite _ _ _ => true | F754_zero _ => true | _ => false end.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN