proposition: Theorem Bone_correct : B2R Bone = 1%R.
proof: Proof. unfold Bone; simpl. set (Hr := binary_round_correct _ _ _ _). unfold Hr; rewrite B2R_SF2B. destruct Hr as (Vz, Hr). revert Hr. fold emin; simpl. rewrite round_generic; [|now apply valid_rnd_N|]. - unfold F2R; simpl; rewrite Rmult_1_r. rewrite Rlt_bool_true. + now intros (Hr, Hr'); rewrite Hr. + rewrite Rabs_R1. change 1%R with (bpow radix2 0); apply bpow_lt. generalize (prec_gt_0 prec) (prec_lt_emax prec emax). lia. - apply generic_format_F2R; intros _. unfold cexp, fexp, FLT_exp, F2R; simpl; rewrite Rmult_1_r, mag_1. unfold emin. generalize (prec_gt_0 prec) (prec_lt_emax prec emax). lia. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative