proposition: Lemma Rlt_bool_float beta b m e : Rlt_bool (FtoR beta b m e) 0 = b.
proof: Proof. destruct e as [|p | p]; destruct b; simpl; apply Rlt_bool_true || apply Rlt_bool_false; try lra. - now apply IZR_lt. - now apply IZR_le. - assert (H1 : (0 < Z.pow_pos beta p)%Z). apply Zpower_pos_gt_0; apply radix_gt_0. revert H1. destruct Z.pow_pos; simpl; try lia; intros _. now apply IZR_lt. - assert (H1 : (0 < Z.pow_pos beta p)%Z). apply Zpower_pos_gt_0; apply radix_gt_0. revert H1. destruct Z.pow_pos; simpl; try lia; intros _. now apply IZR_le. - apply Rdiv_gt_mult_pos. apply IZR_lt. apply Zpower_pos_gt_0; apply radix_gt_0. rewrite Rmult_0_r. now apply IZR_lt. - apply Rdiv_le_mult_pos. apply IZR_lt. apply Zpower_pos_gt_0; apply radix_gt_0. rewrite Rmult_0_l. now apply IZR_le. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic