proposition: Lemma fexp_m_eq_0: (0 = F2R d)%R -> (fexp (mag beta (F2R u)-1) < fexp (mag beta (F2R u))+1)%Z.
proof: Proof. Proof with auto with typeclass_instances. intros Y. assert ((fexp (mag beta (F2R u) - 1) <= fexp (mag beta (F2R u))))%Z. 2: lia. destruct (mag beta x) as (e,He). rewrite Rabs_right in He. 2: now left. assert (e <= fexp e)%Z. apply exp_small_round_0_pos with beta (Zfloor) x... now apply He, Rgt_not_eq. now rewrite <- d_eq, Y. rewrite u_eq, round_UP_small_pos with (ex:=e); trivial. 2: now apply He, Rgt_not_eq. rewrite mag_bpow. ring_simplify (fexp e + 1 - 1)%Z. replace (fexp (fexp e)) with (fexp e). case exists_NE_; intros V. contradict V; rewrite Even_beta; discriminate. rewrite (proj2 (V e)); lia. apply sym_eq, valid_exp; lia. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations