proposition: Lemma ex_shift : forall x e, format x -> (e <= cexp x)%Z -> exists m, (x = IZR m * bpow e)%R.
proof: Proof. Proof with auto with typeclass_instances. intros x e Fx He. exists (Ztrunc (scaled_mantissa beta fexp x)*Zpower beta (cexp x -e))%Z. rewrite Fx at 1; unfold F2R; simpl. rewrite mult_IZR, Rmult_assoc. f_equal. rewrite IZR_Zpower by lia. rewrite <- bpow_plus; f_equal; ring. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations Relative