proposition: Theorem round_round_div_rna_FLT : (emin' <= emin)%Z -> (prec <= prec')%Z -> forall x y, y <> 0 -> FLT_format beta emin prec x -> FLT_format beta emin prec y -> round beta (FLT_exp emin prec) ZnearestA (round beta (FLT_exp emin' prec') ZnearestA (x / y)) = round beta (FLT_exp emin prec) ZnearestA (x / y).
proof: Proof. intros Hemin Hprec x y Nzy Fx Fy. apply round_round_div_beta_odd_rna. - 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. - exact Nzy. - now apply generic_format_FLT. - now apply generic_format_FLT. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core FTZ Double_rounding)