proposition: Lemma mult_bpow_exact_FLX : forall x e, format x -> format (x * bpow e)%R.
proof: Proof. intros x e Fx. destruct (Req_dec x 0) as [Zx|Nzx]. { rewrite Zx, Rmult_0_l; apply generic_format_0. } rewrite Fx. set (mx := Ztrunc _); set (ex := cexp _). pose (f := {| Fnum := mx; Fexp := ex + e |} : float beta). apply (generic_format_F2R' _ _ _ f). { now unfold F2R; simpl; rewrite bpow_plus, Rmult_assoc. } intro Nzmx; unfold mx, ex; rewrite <- Fx. unfold f, ex; simpl; unfold cexp; rewrite (mag_mult_bpow _ _ _ Nzx). unfold FLX_exp; lia. Qed.
imports: Coq(ZArith Reals Lia) Core Operations Plus_error