proposition: Theorem mag_F2R : forall m e : Z, m <> Z0 -> (mag beta (F2R (Float beta m e)) = mag beta (IZR m) + e :> Z)%Z.
proof: Proof. intros m e H. unfold F2R ; simpl. apply mag_mult_bpow. now apply IZR_neq. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Digits