proposition: Theorem F2R_change_exp : forall e' m e : Z, (e' <= e)%Z -> F2R (Float beta m e) = F2R (Float beta (m * Zpower beta (e - e')) e').
proof: Proof. intros e' m e He. unfold F2R. simpl. rewrite mult_IZR, IZR_Zpower, Rmult_assoc. apply f_equal. pattern e at 1 ; replace e with (e - e' + e')%Z by ring. apply bpow_plus. now apply Zle_minus_le_0. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Digits