proposition: Lemma generic_format_F2R' : forall (x : R) (f : float beta), F2R f = x -> (x <> 0%R -> (cexp x <= Fexp f)%Z) -> generic_format x.
proof: Proof. intros x f H1 H2. rewrite <- H1; destruct f as (m,e). apply generic_format_F2R. simpl in *; intros H3. rewrite H1; apply H2. intros Y; apply H3. apply eq_0_F2R with beta e. now rewrite H1. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop