proposition: Lemma pred_pos_plus_ulp_aux3 : forall x, (0 < x)%R -> F x -> let e := mag_val beta x (mag beta x) in x = bpow (e - 1) -> (x - bpow (fexp (e-1)) = 0)%R -> (ulp 0 = x)%R.
proof: Proof. intros x Hx Fx e H1 H2. assert (H3:(x = bpow (fexp (e - 1)))). now apply Rminus_diag_uniq. assert (H4: (fexp (e-1) = e-1)%Z). apply bpow_inj with beta. now rewrite <- H1. unfold ulp; rewrite Req_bool_true; trivial. case negligible_exp_spec. intros K. specialize (K (e-1)%Z). contradict K; lia. intros n Hn. rewrite H3; apply f_equal. case (Zle_or_lt n (e-1)); intros H6. apply valid_exp; lia. apply sym_eq, valid_exp; lia. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop