proposition: Lemma le_pred_pos_lt : forall x y, F x -> F y -> (0 <= x < y)%R -> (x <= pred_pos y)%R.
proof: Proof. Proof with auto with typeclass_instances. intros x y Fx Fy H. case (proj1 H); intros V. assert (Zy:(0 < y)%R). apply Rle_lt_trans with (1:=proj1 H). apply H. assert (Zp: (0 < pred y)%R). assert (Zp:(0 <= pred y)%R). apply pred_ge_0 ; trivial. destruct Zp; trivial. generalize H0. rewrite pred_eq_pos;[idtac|now left]. unfold pred_pos. destruct (mag beta y) as (ey,Hey); simpl. case Req_bool_spec; intros Hy2. intros Hy3. assert (ey-1 = fexp (ey -1))%Z. apply bpow_inj with beta. rewrite <- Hy2, <- Rplus_0_l, Hy3. ring. assert (Zx: (x <> 0)%R). now apply Rgt_not_eq. destruct (mag beta x) as (ex,Hex). specialize (Hex Zx). assert (ex <= ey)%Z. apply bpow_lt_bpow with beta. apply Rle_lt_trans with (1:=proj1 Hex). apply Rlt_trans with (Rabs y). rewrite 2!Rabs_right. apply H. now apply Rgt_ge. now apply Rgt_ge. apply Hey. now apply Rgt_not_eq. case (Zle_lt_or_eq _ _ H2); intros Hexy. assert (fexp ex = fexp (ey-1))%Z. apply valid_exp. lia. rewrite <- H1. lia. absurd (0 < Ztrunc (scaled_mantissa beta fexp x) < 1)%Z. lia. split. apply gt_0_F2R with beta (cexp beta fexp x). now rewrite <- Fx. apply lt_IZR. apply Rmult_lt_reg_r with (bpow (cexp beta fexp x)). apply bpow_gt_0. replace (IZR (Ztrunc (scaled_mantissa beta fexp x)) * bpow (cexp beta fexp x))%R with x. rewrite Rmult_1_l. unfold cexp. rewrite mag_unique with beta x ex. rewrite H3,<-H1, <- Hy2. apply H. exact Hex. absurd (y <= x)%R. now apply Rlt_not_le. rewrite Rabs_right in Hex. apply Rle_trans with (2:=proj1 Hex). rewrite Hexy, Hy2. now apply Rle_refl. now apply Rgt_ge. intros Hy3. assert (y = bpow (fexp ey))%R. apply Rminus_diag_uniq. rewrite Hy3. rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq]. unfold cexp. rewrite (mag_unique beta y ey); trivial. apply Hey. now apply Rgt_not_eq. contradict Hy2. rewrite H1. apply f_equal. apply Zplus_reg_l with 1%Z. ring_simplify. apply trans_eq with (mag beta y). apply sym_eq; apply mag_unique. rewrite H1, Rabs_right. split. apply bpow_le. lia. apply bpow_lt. lia. apply Rle_ge; apply bpow_ge_0. apply mag_unique. apply Hey. now apply Rgt_not_eq. case (Rle_or_lt (ulp (pred_pos y)) (y-x)); intros H1. apply Rplus_le_reg_r with (-x + ulp (pred_pos y))%R. ring_simplify (x+(-x+ulp (pred_pos y)))%R. apply Rle_trans with (1:=H1). rewrite <- (pred_pos_plus_ulp y) at 1; trivial. apply Req_le; ring. replace x with (y-(y-x))%R by ring. rewrite <- pred_eq_pos;[idtac|now left]. rewrite <- round_DN_minus_eps_pos with (eps:=(y-x)%R); try easy. ring_simplify (y-(y-x))%R. apply Req_le. apply sym_eq. apply round_generic... split; trivial. now apply Rlt_Rminus. rewrite pred_eq_pos;[idtac|now left]. now apply Rlt_le. rewrite <- V; apply pred_pos_ge_0; trivial. apply Rle_lt_trans with (1:=proj1 H); apply H. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop