proposition: Lemma pred_pos_lt_id : forall x, (x <> 0)%R -> (pred_pos x < x)%R.
proof: Proof. intros x Zx. unfold pred_pos. case Req_bool_spec; intros H. rewrite <- Rplus_0_r. apply Rplus_lt_compat_l. rewrite <- Ropp_0. apply Ropp_lt_contravar. apply bpow_gt_0. rewrite <- Rplus_0_r. apply Rplus_lt_compat_l. rewrite <- Ropp_0. apply Ropp_lt_contravar. rewrite ulp_neq_0; trivial. apply bpow_gt_0. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop