proposition: Lemma sqrt_DN_correct : forall p x, valid_lb x = true -> (valid_lb (sqrt_DN p x) = true /\ le_lower (toX (sqrt_DN p x)) (Xsqrt (toX x))).
proof: Proof. intros p x _; split; [easy|]. unfold sqrt_DN. rewrite (@Fsqrt_correct radix). unfold toX. case FtoX; [easy|intro rx]. unfold Xsqrt, Xsqrt_nan, Xsqrt', Xsqrt_nan'. case is_negative_spec; [easy|intros _]. unfold le_lower, Xneg; simpl; apply Ropp_le_contravar. now apply Generic_fmt.round_DN_pt, FLX.FLX_exp_valid. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Zaux Raux) Xreal Basic Generic Generic_proof Sig