proposition: Theorem succ_gt_id : forall x, (x <> 0)%R -> (x < succ x)%R.
proof: Proof. intros x Zx; unfold succ. case Rle_bool_spec; intros Hx. pattern x at 1; rewrite <- (Rplus_0_r x). apply Rplus_lt_compat_l. rewrite ulp_neq_0; trivial. apply bpow_gt_0. pattern x at 1; rewrite <- (Ropp_involutive x). apply Ropp_lt_contravar. apply pred_pos_lt_id. auto with real. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop