proposition: Theorem round_round_plus_radix_ge_3_FLT : (3 <= beta)%Z -> forall choice1 choice2, (emin' <= emin)%Z -> (2 * prec <= prec')%Z -> forall x y, FLT_format beta emin prec x -> FLT_format beta emin prec y -> round_round_eq (FLT_exp emin prec) (FLT_exp emin' prec') choice1 choice2 (x + y).
proof: Proof. intros Hbeta choice1 choice2 Hemin Hprec x y Fx Fy. apply round_round_plus_radix_ge_3. - exact Hbeta. - now apply FLT_exp_valid. - now apply FLT_exp_valid. - now apply FLT_round_round_plus_radix_ge_3_hyp. - now apply generic_format_FLT. - now apply generic_format_FLT. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ