proposition: Theorem succ_le_inv: forall x y, F x -> F y -> (succ x <= succ y)%R -> (x <= y)%R.
proof: Proof. intros x y Fx Fy Hxy. rewrite <- (pred_succ x), <- (pred_succ y); try assumption. apply pred_le; trivial; now apply generic_format_succ. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop