proposition: Theorem generic_format_0 : generic_format 0.
proof: Proof. unfold generic_format, scaled_mantissa. rewrite Rmult_0_l. now rewrite Ztrunc_IZR, F2R_0. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop