proposition: Theorem generic_format_discrete : forall x m, let e := cexp x in (F2R (Float beta m e) < x < F2R (Float beta (m + 1) e))%R -> ~ generic_format x.
proof: Proof. intros x m e (Hx,Hx2) Hf. apply Rlt_not_le with (1 := Hx2). clear Hx2. rewrite Hf. fold e. apply F2R_le. apply Zlt_le_succ. apply lt_IZR. rewrite <- scaled_mantissa_generic with (1 := Hf). apply Rmult_lt_reg_r with (bpow e). apply bpow_gt_0. now rewrite scaled_mantissa_mult_bpow. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop