proposition: Theorem round_DN_minus_eps_pos : forall x, (0 < x)%R -> F x -> forall eps, (0 < eps <= ulp (pred x))%R -> round beta fexp Zfloor (x - eps) = pred x.
proof: Proof. intros x Hpx Fx eps. rewrite pred_eq_pos;[intros Heps|now left]. replace (x-eps)%R with (pred_pos x + (ulp (pred_pos x)-eps))%R. 2: pattern x at 3; rewrite <- (pred_pos_plus_ulp x); trivial. 2: ring. rewrite round_DN_plus_eps_pos; trivial. now apply pred_pos_ge_0. now apply generic_format_pred_pos. split. apply Rle_0_minus. now apply Heps. rewrite <- Rplus_0_r. apply Rplus_lt_compat_l. rewrite <- Ropp_0. apply Ropp_lt_contravar. now apply Heps. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop