proposition: Theorem round_DN_minus_eps: forall x, F x -> forall eps, (0 < eps <= if (Rle_bool x 0) then (ulp x) else (ulp (pred x)))%R -> round beta fexp Zfloor (x - eps) = pred x.
proof: Proof. intros x Fx eps Heps. replace (x-eps)%R with (-(-x+eps))%R by ring. rewrite round_DN_opp. unfold pred; apply f_equal. pattern (-x)%R at 1; rewrite <- (pred_succ (-x)). apply round_UP_pred_plus_eps. now apply generic_format_succ, generic_format_opp. rewrite pred_succ. rewrite ulp_opp. generalize Heps; case (Rle_bool_spec x 0); intros H1 H2. rewrite Rle_bool_false; trivial. case H1; intros H1'. apply Rlt_le_trans with (-x)%R. now apply Ropp_0_gt_lt_contravar. apply succ_ge_id. rewrite H1', Ropp_0, succ_eq_pos;[idtac|now right]. rewrite Rplus_0_l. apply Rlt_le_trans with (1:=proj1 H2). rewrite H1' in H2; apply H2. rewrite Rle_bool_true. now rewrite succ_opp, ulp_opp. rewrite succ_opp. rewrite <- Ropp_0; apply Ropp_le_contravar. now apply pred_ge_0. now apply generic_format_opp. now apply generic_format_opp. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop