proposition: Theorem succ_pred : forall x, F x -> succ (pred x) = x.
proof: Proof. intros x Fx. destruct (Rle_or_lt 0 x) as [[Hx|Hx]|Hx]. now apply succ_pred_pos. rewrite <- Hx. rewrite pred_0, succ_opp, pred_ulp_0. apply Ropp_0. unfold pred. rewrite succ_opp, pred_succ_pos. apply Ropp_involutive. 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