proposition: Lemma pred_succ_pos : forall x, F x -> (0 < x)%R -> pred (succ x) = x.
proof: Proof. intros x Fx Hx. apply Rle_antisym. - apply Rnot_lt_le. intros H. apply succ_le_lt with (1 := Fx) in H. revert H. apply Rlt_not_le. apply pred_lt_id. apply Rgt_not_eq. apply Rlt_le_trans with (1 := Hx). apply succ_ge_id. now apply generic_format_pred, generic_format_succ. - apply pred_ge_gt with (1 := Fx). now apply generic_format_succ. apply succ_gt_id. now apply Rgt_not_eq. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop