proposition: Theorem mag_F2R_Zdigits : forall m e, m <> Z0 -> (mag beta (F2R (Float beta m e)) = Zdigits beta m + e :> Z)%Z.
proof: Proof. intros m e Hm. rewrite mag_F2R with (1 := Hm). apply (f_equal (fun v => Zplus v e)). apply sym_eq. now apply Zdigits_mag. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Digits