proposition: Lemma generic_format_plus_prec : forall fexp, (forall e, (fexp e <= e - prec)%Z) -> forall x y (fx fy: float beta), (x = F2R fx)%R -> (y = F2R fy)%R -> (Rabs (x+y) < bpow (prec+Fexp fx))%R -> (Rabs (x+y) < bpow (prec+Fexp fy))%R -> generic_format beta fexp (x+y)%R.
proof: Proof. intros fexp Hfexp x y fx fy Hx Hy H1 H2. case (Req_dec (x+y) 0); intros H. rewrite H; apply generic_format_0. rewrite Hx, Hy, <- F2R_plus. apply generic_format_F2R. intros _. change (F2R _) with (F2R (Fplus fx fy)). apply Z.le_trans with (Z.min (Fexp fx) (Fexp fy)). rewrite F2R_plus, <- Hx, <- Hy. unfold cexp. apply Z.le_trans with (1:=Hfexp _). apply Zplus_le_reg_l with prec; ring_simplify. apply mag_le_bpow with (1 := H). now apply Z.min_case. rewrite <- Fexp_Fplus. apply Z.le_refl. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations Relative Sterbenz Mult_error