proposition: Theorem mag_generic_gt : forall x, (x <> 0)%R -> generic_format x -> (cexp x < mag beta x)%Z.
proof: Proof. intros x Zx Gx. apply Znot_ge_lt. unfold cexp. destruct (mag beta x) as (ex,Ex) ; simpl. specialize (Ex Zx). intros H. apply Z.ge_le in H. generalize (scaled_mantissa_lt_1 x ex (proj2 Ex) H). contradict Zx. rewrite Gx. replace (Ztrunc (scaled_mantissa x)) with Z0. apply F2R_0. cut (Z.abs (Ztrunc (scaled_mantissa x)) < 1)%Z. clear ; lia. apply lt_IZR. rewrite abs_IZR. now rewrite <- scaled_mantissa_generic. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop