proposition: Theorem round_round_sqrt_FTZ : (4 <= beta)%Z -> forall choice1 choice2, (2 * (emin' + prec') <= emin + prec <= 1)%Z -> (2 * prec + 2 <= prec')%Z -> forall x, FTZ_format beta emin prec x -> round_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec') choice1 choice2 (sqrt x).
proof: Proof. intros Hbeta choice1 choice2 Hemin Hprec x Fx. apply round_round_sqrt. - now apply FTZ_exp_valid. - now apply FTZ_exp_valid. - now apply FTZ_round_round_sqrt_hyp. - now apply generic_format_FTZ. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ