proposition: Lemma round_FLT_plus_ge' : forall x y e, generic_format beta (FLT_exp emin prec) x -> generic_format beta (FLT_exp emin prec) y -> (x <> 0%R -> (bpow (e+prec) <= Rabs x)%R) -> (x = 0%R -> y <> 0%R -> (bpow e <= Rabs y)%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 H1 H2 H3. case (Req_dec x 0); intros H4. case (Req_dec y 0); intros H5. contradict H3. rewrite H4, H5, Rplus_0_l; apply round_0... rewrite H4, Rplus_0_l. rewrite round_generic... apply round_FLT_plus_ge; try easy. now apply H1. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations Relative