proposition: Theorem pred_eq_pos : forall x, (0 <= x)%R -> pred x = pred_pos x.
proof: Proof. intros x Hx; unfold pred, succ. case Rle_bool_spec; intros Hx'. assert (K:(x = 0)%R). apply Rle_antisym; try assumption. apply Ropp_le_cancel. now rewrite Ropp_0. rewrite K; unfold pred_pos. rewrite Req_bool_false. 2: apply Rlt_not_eq, bpow_gt_0. rewrite Ropp_0; ring. now rewrite 2!Ropp_involutive. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop