proposition: Theorem F2R_prec_normalize : forall m e e' p : Z, (Z.abs m < Zpower beta p)%Z -> (bpow (e' - 1)%Z <= Rabs (F2R (Float beta m e)))%R -> F2R (Float beta m e) = F2R (Float beta (m * Zpower beta (e - e' + p)) (e' - p)).
proof: Proof. intros m e e' p Hm Hf. assert (Hp: (0 <= p)%Z). destruct p ; try easy. now elim (Zle_not_lt _ _ (Zabs_pos m)). replace (e - e' + p)%Z with (e - (e' - p))%Z by ring. apply F2R_change_exp. cut (e' - 1 < e + p)%Z. lia. apply (lt_bpow beta). apply Rle_lt_trans with (1 := Hf). rewrite <- F2R_Zabs, Zplus_comm, bpow_plus. apply Rmult_lt_compat_r. apply bpow_gt_0. rewrite <- IZR_Zpower. now apply IZR_lt. exact Hp. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Digits