proposition: Theorem pred_le : forall x y, F x -> F y -> (x <= y)%R -> (pred x <= pred y)%R.
proof: Proof. intros x y Fx Fy [Hxy| ->]. 2: apply Rle_refl. apply pred_ge_gt with (2 := Fy). now apply generic_format_pred. apply Rle_lt_trans with (2 := Hxy). apply pred_le_id. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop