proposition: Theorem generic_format_succ : forall x, F x -> F (succ x).
proof: Proof. intros x Fx. unfold succ; case Rle_bool_spec; intros Zx. destruct Zx as [Zx|Zx]. now apply generic_format_succ_aux1. rewrite <- Zx, Rplus_0_l. apply generic_format_ulp_0. apply generic_format_opp. apply generic_format_pred_pos. now apply generic_format_opp. now apply Ropp_0_gt_lt_contravar. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop