proposition: Lemma pred_pos_ge_0 : forall x, (0 < x)%R -> F x -> (0 <= pred_pos x)%R.
proof: Proof. intros x Zx Fx. unfold pred_pos. case Req_bool_spec; intros H. apply Rle_0_minus. rewrite H. apply bpow_le. destruct (mag beta x) as (ex,Ex) ; simpl. rewrite mag_bpow. ring_simplify (ex - 1 + 1 - 1)%Z. apply generic_format_bpow_inv with beta; trivial. simpl in H. rewrite <- H; assumption. apply Rle_0_minus. now apply ulp_le_id. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop