proposition: Lemma succ_le_lt_aux: forall x y, F x -> F y -> (0 <= x)%R -> (x < y)%R -> (succ x <= y)%R.
proof: Proof. Proof with auto with typeclass_instances. intros x y Hx Hy Zx H. rewrite succ_eq_pos; trivial. case (Rle_or_lt (ulp x) (y-x)); intros H1. apply Rplus_le_reg_r with (-x)%R. now ring_simplify (x+ulp x + -x)%R. replace y with (x+(y-x))%R by ring. absurd (x < y)%R. 2: apply H. apply Rle_not_lt; apply Req_le. rewrite <- round_DN_plus_eps_pos with (eps:=(y-x)%R); try easy. ring_simplify (x+(y-x))%R. apply sym_eq. apply round_generic... split; trivial. apply Rlt_le; now apply Rlt_Rminus. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop