proposition: Lemma pred_pos_plus_ulp_aux1 : forall x, (0 < x)%R -> F x -> x <> bpow (mag beta x - 1) -> ((x - ulp x) + ulp (x-ulp x) = x)%R.
proof: Proof. intros x Zx Fx Hx. replace (ulp (x - ulp x)) with (ulp x). ring. assert (H : x <> 0%R) by now apply Rgt_not_eq. assert (H' : x <> bpow (cexp beta fexp x)). unfold cexp ; intros M. case_eq (mag beta x); intros ex Hex T. assert (Lex:(mag_val beta x (mag beta x) = ex)%Z). rewrite T; reflexivity. rewrite Lex in *. clear T; simpl in *; specialize (Hex H). rewrite Rabs_pos_eq in Hex by now apply Rlt_le. assert (ex - 1 < fexp ex < ex)%Z. split ; apply (lt_bpow beta) ; rewrite <- M by easy. lra. apply Hex. lia. rewrite 2!ulp_neq_0 by lra. apply f_equal. unfold cexp ; apply f_equal. case_eq (mag beta x); intros ex Hex T. assert (Lex:(mag_val beta x (mag beta x) = ex)%Z). rewrite T; reflexivity. rewrite Lex in *; simpl in *; clear T. specialize (Hex H). apply sym_eq, mag_unique. rewrite Rabs_right. rewrite Rabs_right in Hex. 2: apply Rle_ge; apply Rlt_le; easy. split. destruct Hex as ([H1|H1],H2). apply Rle_trans with (x-ulp x)%R. apply id_m_ulp_ge_bpow; trivial. rewrite ulp_neq_0; trivial. rewrite ulp_neq_0; trivial. right; unfold cexp; now rewrite Lex. lra. apply Rle_lt_trans with (2:=proj2 Hex). rewrite <- Rplus_0_r. apply Rplus_le_compat_l. rewrite <- Ropp_0. apply Ropp_le_contravar. apply bpow_ge_0. apply Rle_ge. apply Rle_0_minus. rewrite Fx. unfold F2R, cexp; simpl. rewrite Lex. pattern (bpow (fexp ex)) at 1; rewrite <- Rmult_1_l. apply Rmult_le_compat_r. apply bpow_ge_0. apply IZR_le, (Zlt_le_succ 0). apply gt_0_F2R with beta (cexp beta fexp x). now rewrite <- Fx. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop