proposition: Theorem round_FLT_plus_ge : forall x y e, generic_format beta (FLT_exp emin prec) x -> generic_format beta (FLT_exp emin prec) y -> (bpow (e + prec) <= Rabs x)%R -> round beta (FLT_exp emin prec) rnd (x + y) <> 0%R -> (bpow e <= Rabs (round beta (FLT_exp emin prec) rnd (x + y)))%R.
proof: Proof. Proof with auto with typeclass_instances. intros x y e Fx Fy He KK. assert (Zx: x <> 0%R). contradict He. apply Rlt_not_le; rewrite He, Rabs_R0. apply bpow_gt_0. apply Rle_trans with (ulp beta (FLT_exp emin prec) (x/IZR beta)). 2: apply round_plus_ge_ulp... rewrite ulp_neq_0. unfold cexp. rewrite <- mag_minus1; try assumption. unfold FLT_exp; apply bpow_le. apply Z.le_trans with (2:=Z.le_max_l _ _). destruct (mag beta x) as (n,Hn); simpl. cut (e + prec < n)%Z. lia. apply lt_bpow with beta. apply Rle_lt_trans with (1:=He). now apply Hn. apply Rmult_integral_contrapositive_currified; try assumption. apply Rinv_neq_0_compat. apply Rgt_not_eq. apply radix_pos. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations Relative