proposition: Theorem pred_ge_gt : forall x y, F x -> F y -> (x < y)%R -> (x <= pred y)%R.
proof: Proof. intros x y Fx Fy Hxy. rewrite <- (Ropp_involutive x). unfold pred; apply Ropp_le_contravar. apply succ_le_lt. now apply generic_format_opp. now apply generic_format_opp. now apply Ropp_lt_contravar. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop