proposition: Fact ex12 : generic_format r phi 0.
proof: Proof. unfold generic_format, F2R, scaled_mantissa; simpl. assert (H : 0 * bpow r (- cexp r phi 0) = 0). simpl; ring. rewrite H, Ztrunc_IZR; simpl; ring. Qed.
imports: Psatz ZArith Reals Flocq(FTZ Core Operations)