proposition: Theorem FLT_format_plus_small: forall x y, generic_format beta (FLT_exp emin prec) x -> generic_format beta (FLT_exp emin prec) y -> (Rabs (x+y) <= bpow (prec+emin))%R -> generic_format beta (FLT_exp emin prec) (x+y).
proof: Proof. Proof with auto with typeclass_instances. intros x y Fx Fy H. apply generic_format_FLT_FIX... rewrite Zplus_comm; assumption. apply generic_format_FIX_FLT, FIX_format_generic in Fx. apply generic_format_FIX_FLT, FIX_format_generic in Fy. destruct Fx as [nx H1x H2x]. destruct Fy as [ny H1y H2y]. apply generic_format_FIX. exists (Float beta (Fnum nx+Fnum ny)%Z emin). rewrite H1x,H1y; unfold F2R; simpl. rewrite H2x, H2y. rewrite plus_IZR; ring. easy. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations Relative