proposition: Lemma succ_pred_pos : forall x, F x -> (0 < x)%R -> succ (pred x) = x.
proof: Proof. intros x Fx Hx. rewrite pred_eq_pos by now left. rewrite succ_eq_pos by now apply pred_pos_ge_0. now apply pred_pos_plus_ulp. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop