proposition: Theorem Beqb_refl : forall f, Beqb f f = negb (is_nan f).
proof: Proof. intros f. generalize (fun H => Beqb_correct f f H H). destruct f as [s|[|]| |s m e H] ; try easy. intros ->. 2: easy. now apply Req_bool_true. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative