proposition: Lemma round_round_plus_radix_ge_3_aux2 : (3 <= beta)%Z -> forall (fexp1 fexp2 : Z -> Z), Valid_exp fexp1 -> Valid_exp fexp2 -> forall (choice1 choice2 : Z -> bool), round_round_plus_radix_ge_3_hyp fexp1 fexp2 -> forall x y, 0 < y -> y <= x -> generic_format beta fexp1 x -> generic_format beta fexp1 y -> round_round_eq fexp1 fexp2 choice1 choice2 (x + y).
proof: Proof. intros Hbeta fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Py Hyx Fx Fy. assert (Px := Rlt_le_trans 0 y x Py Hyx). unfold round_round_eq. destruct (Zle_or_lt (mag y) (fexp1 (mag x) - 1)) as [Hly|Hly]. - now apply round_round_plus_radix_ge_3_aux1. - rewrite (round_generic beta fexp2). + reflexivity. + now apply valid_rnd_N. + assert (Hf1 : (fexp1 (mag x) <= mag y)%Z) by lia. now apply (round_round_plus_radix_ge_3_aux0 fexp1). Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ