proposition: Theorem generic_format_F2R : forall m e, ( m <> 0 -> cexp (F2R (Float beta m e)) <= e )%Z -> generic_format (F2R (Float beta m e)).
proof: Proof. intros m e. destruct (Z.eq_dec m 0) as [Zm|Zm]. intros _. rewrite Zm, F2R_0. apply generic_format_0. unfold generic_format, scaled_mantissa. set (e' := cexp (F2R (Float beta m e))). intros He. specialize (He Zm). unfold F2R at 3. simpl. rewrite F2R_change_exp with (1 := He). apply F2R_eq. rewrite Rmult_assoc, <- bpow_plus, <- IZR_Zpower, <- mult_IZR. now rewrite Ztrunc_IZR. now apply Zle_left. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop