proposition: Lemma pred_pos_plus_ulp_aux2 : 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 -> ((x - bpow (fexp (e-1))) + ulp (x - bpow (fexp (e-1))) = x)%R.
proof: Proof. intros x Zx Fx e Hxe Zp. replace (ulp (x - bpow (fexp (e - 1)))) with (bpow (fexp (e - 1))). ring. assert (He:(fexp (e-1) <= e-1)%Z). apply generic_format_bpow_inv with beta; trivial. rewrite <- Hxe; assumption. case (Zle_lt_or_eq _ _ He); clear He; intros He. rewrite ulp_neq_0; trivial. apply f_equal. unfold cexp ; apply f_equal. apply sym_eq. apply mag_unique. rewrite Rabs_right. split. apply Rplus_le_reg_l with (bpow (fexp (e-1))). ring_simplify. apply Rle_trans with (bpow (e - 2) + bpow (e - 2))%R. apply Rplus_le_compat; apply bpow_le; lia. apply Rle_trans with (2*bpow (e - 2))%R;[right; ring|idtac]. apply Rle_trans with (bpow 1*bpow (e - 2))%R. apply Rmult_le_compat_r. apply bpow_ge_0. replace (bpow 1) with (IZR beta). apply IZR_le. apply <- Zle_is_le_bool. now destruct beta. simpl. unfold Zpower_pos; simpl. now rewrite Zmult_1_r. rewrite <- bpow_plus. replace (1+(e-2))%Z with (e-1)%Z by ring. now right. rewrite <- Rplus_0_r, Hxe. apply Rplus_lt_compat_l. rewrite <- Ropp_0. apply Ropp_lt_contravar. apply bpow_gt_0. apply Rle_ge; apply Rle_0_minus. rewrite Hxe. apply bpow_le. lia. contradict Zp. rewrite Hxe, He; ring. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop