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