proposition: Theorem pred_bpow : forall e, pred (bpow e) = (bpow e - bpow (fexp e))%R.
proof: Proof. intros e. rewrite pred_eq_pos by apply bpow_ge_0. unfold pred_pos. rewrite mag_bpow. replace (e + 1 - 1)%Z with e by ring. now rewrite Req_bool_true. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop