proposition: Theorem succ_le_lt: forall x y, F x -> F y -> (x < y)%R -> (succ x <= y)%R.
proof: Proof. Proof with auto with typeclass_instances. intros x y Fx Fy H. destruct (Rle_or_lt 0 x) as [Hx|Hx]. now apply succ_le_lt_aux. unfold succ; rewrite Rle_bool_false; try assumption. case (Rle_or_lt y 0); intros Hy. rewrite <- (Ropp_involutive y). apply Ropp_le_contravar. apply le_pred_pos_lt. now apply generic_format_opp. now apply generic_format_opp. split. rewrite <- Ropp_0; now apply Ropp_le_contravar. now apply Ropp_lt_contravar. apply Rle_trans with (-0)%R. apply Ropp_le_contravar. apply pred_pos_ge_0. rewrite <- Ropp_0; now apply Ropp_lt_contravar. now apply generic_format_opp. rewrite Ropp_0; now left. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop