proposition: Theorem round_round_sqrt_beta_odd_FLT : forall choice1 choice2, (emin' <= emin)%Z -> (prec <= prec')%Z -> forall x, FLT_format beta emin prec x -> round_round_eq beta (FLT_exp emin prec) (FLT_exp emin' prec') choice1 choice2 (sqrt x).
proof: Proof. intros choice1 choice2 Hemin Hprec x Fx. apply round_round_sqrt_beta_odd. - now apply FLT_exp_valid. - now apply FLT_exp_valid. - intro ex; unfold FLT_exp. generalize (Zmax_spec (ex - prec) emin). generalize (Zmax_spec (ex - prec') emin'). lia. - now apply generic_format_FLT. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core FTZ Double_rounding)