proposition: Fact ext2 x : ~ generic_format r phi x -> round r phi Zceil x = round r phi Zfloor x + ulp r phi x.
proof: Proof. intros H. assert (NZx : x <> 0). contradict H; rewrite H; apply generic_format_0. rewrite ulp_neq_0; auto. unfold round, F2R; simpl. rewrite Zceil_floor_neq; rewrite ?plus_IZR; simpl; try ring. contradict H. unfold generic_format, F2R; simpl. rewrite <- H, Ztrunc_IZR, H. rewrite scaled_mantissa_mult_bpow; auto. Qed.
imports: Psatz ZArith Reals SpecFloat Flocq(FTZ Core Operations BinarySingleNaN Binary Bits)