proposition: Lemma FLT_iff_generic : forall p x, FLT x p <-> generic_format radix2 (FLX_exp (Zpos p)) x.
proof: Proof. intros p x. split. intros ((m,e),(H1,H2)). apply generic_format_FLX. exists (Float radix2 m e). now apply sym_eq. exact H2. intros H. destruct (@FLX_format_generic _ (Zpos p) (refl_equal Lt) _ H) as ((m,e),H1,H2). now exists (Float2 m e) ; repeat split. Qed.
imports: Coq(ZArith Reals) Flocq(Zaux Raux Defs Digits Float_prop Generic_fmt FIX FLX) Gappa_definitions Gappa_dyadic