proposition: Theorem ulp_bpow : forall e, ulp (bpow e) = bpow (fexp (e + 1)).
proof: Proof. intros e. rewrite ulp_neq_0. apply f_equal. apply cexp_fexp. rewrite Rabs_pos_eq. split. ring_simplify (e + 1 - 1)%Z. apply Rle_refl. apply bpow_lt. apply Zlt_succ. apply bpow_ge_0. apply Rgt_not_eq, Rlt_gt, bpow_gt_0. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop