proposition: Theorem succ_ge_id : forall x, (x <= succ x)%R.
proof: Proof. intros x; case (Req_dec x 0). intros V; rewrite V. unfold succ; rewrite Rle_bool_true;[idtac|now right]. rewrite Rplus_0_l; apply ulp_ge_0. intros; left; now apply succ_gt_id. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop