proposition: Lemma FIX_iff_generic : forall k x, FIX x k <-> generic_format radix2 (FIX_exp k) x.
proof: Proof. intros k x. split. intros ((m,e),(H1,H2)). rewrite <- H1. now apply generic_format_F2R. intros H. destruct (FIX_format_generic _ _ _ H) as ((m,e),H1,H2). exists (Float2 m e) ; repeat split. easy. rewrite <- H2. apply Z.le_refl. Qed.
imports: Coq(ZArith Reals) Flocq(Zaux Raux Defs Digits Float_prop Generic_fmt FIX FLX) Gappa_definitions Gappa_dyadic