proposition: Lemma FIX_format_IZR : forall beta x, FIX_format beta 0 (IZR x).
proof: Proof. intros beta x. exists (Float beta x 0). apply sym_eq, Rmult_1_r. apply eq_refl. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core) Gappa(Gappa_tactic)