proposition: Theorem sqrt_equiv : forall x, Prim2B (sqrt x) = Bsqrt mode_NE (Prim2B x).
proof: Proof. intro x. apply B2Prim_inj. rewrite B2Prim_Prim2B. apply Prim2SF_inj. rewrite Prim2SF_B2Prim. rewrite sqrt_spec. rewrite <-B2SF_Prim2B. case Prim2B as [sx|sx| |sx mx ex Bx]; [now (trivial || case sx).. | ]. case sx; [reflexivity | ]. simpl. rewrite B2SF_SF2B. set (melz := SFsqrt_core_binary _ _ _ _). case melz as [[mz ez] lz]. apply binary_round_aux_equiv. Qed.
imports: Int63Compat Coq(ZArith Reals Floats SpecFloat) Zaux BinarySingleNaN