proposition: Theorem pred_ulp_0 : pred (ulp 0) = 0%R.
proof: Proof. rewrite pred_eq_pos. 2: apply ulp_ge_0. unfold ulp; rewrite Req_bool_true; trivial. case negligible_exp_spec'. intros [H1 _]; rewrite H1. unfold pred_pos; rewrite Req_bool_false. 2: apply Rlt_not_eq, bpow_gt_0. unfold ulp; rewrite Req_bool_true; trivial. rewrite H1; ring. intros (n,(H1,H2)); rewrite H1. unfold pred_pos. rewrite mag_bpow. replace (fexp n + 1 - 1)%Z with (fexp n) by ring. rewrite Req_bool_true; trivial. apply Rminus_diag_eq, f_equal. apply sym_eq, valid_exp; lia. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop