proposition: Lemma mag_m_0: (0 = F2R d)%R -> (mag beta m =mag beta (F2R u)-1:>Z)%Z.
proof: Proof. Proof with auto with typeclass_instances. intros Y. apply mag_unique_pos. unfold m; rewrite <- Y, Rplus_0_l. rewrite u_eq. destruct (mag beta x) as (e,He). rewrite Rabs_pos_eq in He by now apply Rlt_le. rewrite round_UP_small_pos with (ex:=e). rewrite mag_bpow. ring_simplify (fexp e + 1 - 1)%Z. split. unfold Zminus; rewrite bpow_plus. unfold Rdiv; apply Rmult_le_compat_l. apply bpow_ge_0. simpl; unfold Z.pow_pos; simpl. rewrite Zmult_1_r; apply Rinv_le. exact Rlt_0_2. apply IZR_le. specialize (radix_gt_1 beta). lia. apply Rlt_le_trans with (bpow (fexp e)*1)%R. 2: right; ring. unfold Rdiv; apply Rmult_lt_compat_l. apply bpow_gt_0. lra. now apply He, Rgt_not_eq. apply exp_small_round_0_pos with beta (Zfloor) x... now apply He, Rgt_not_eq. now rewrite <- d_eq, Y. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations