proposition: Lemma sqrt_UP_correct : forall p x, valid_ub (sqrt_UP p x) = true /\ le_upper (Xsqrt (toX x)) (toX (sqrt_UP p x)).
proof: Proof. intros p x; split; [reflexivity|]. unfold sqrt_UP. rewrite sqrt_correct. unfold Xround, Xlift. case toX; [easy|intro rx]. unfold Xsqrt', Xsqrt_nan'. case is_negative_spec; [easy|intros _]. now apply Generic_fmt.round_UP_pt, FLX.FLX_exp_valid. Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig