proposition: Theorem Bsqrt_correct : forall sqrt_nan m x, B2R (Bsqrt sqrt_nan m x) = round radix2 fexp (round_mode m) (sqrt (B2R x)) /\ is_finite (Bsqrt sqrt_nan m x) = match x with B754_zero _ => true | B754_finite false _ _ _ => true | _ => false end /\ (is_nan (Bsqrt sqrt_nan m x) = false -> Bsign (Bsqrt sqrt_nan m x) = Bsign x).
proof: Proof. intros sqrt_nan mode x. generalize (Bsqrt_correct prec emax _ _ mode (B2BSN x)). replace (BinarySingleNaN.Bsqrt _ _) with (B2BSN (Bsqrt sqrt_nan mode x)) by apply B2BSN_BSN2B. intros H. destruct x as [sx|[|]|sx plx Hplx|sx mx ex Hx] ; try easy. now destruct Bsqrt. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN